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

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

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