基于IP復(fù)用的片上系統(tǒng)的形式化驗證技術(shù)研究.pdf

1、由于片上系統(tǒng)(SoC)的規(guī)模和功能在不斷膨脹,為了保證設(shè)計的正確性,縮短設(shè)計的周期,在設(shè)計過程中的驗證就變得越來越重要,也更為復(fù)雜,向業(yè)界提出了挑戰(zhàn)。
　　SoC的驗證包括模擬、仿真和形式化驗證。本文主要針對基于IP復(fù)用的SoC的形式化驗證技術(shù)進行研究,所取得的主要成果有:
　　(1)針對SoC中的AMBA AHB總線協(xié)議,提出了一種可以借鑒的形式化建模與驗證方法。對AHB總線協(xié)議進行了形式化規(guī)格;建立了與其規(guī)格對應(yīng)的有限自

2、動機模型;建立協(xié)議的SMV模型,以及應(yīng)用CTL對屬性進行了形式描述,借助符號模型檢驗器SMV對總線無饑餓屬性進行驗證。
　　(2)在分析現(xiàn)有Petri網(wǎng)技術(shù)的基礎(chǔ)上,提出一種適于嵌入式系統(tǒng)建模的擴展流關(guān)系Petri網(wǎng)(EFPN),并對其結(jié)構(gòu)和動態(tài)行為規(guī)則進行了定義。采用EFPN對乘法器進行了建模,并與另外幾種對應(yīng)的Petri網(wǎng)模型進行了比較;以移動電話系統(tǒng)為例,將EFPN有效地應(yīng)用于膠合邏輯的建模。
　　(3)針對已經(jīng)建立的