在數(shù)字系統(tǒng)設(shè)計(jì)中斷言驗(yàn)證的研究.pdf

1、隨著微電子技術(shù)的高速發(fā)展，人們對電子產(chǎn)品的強(qiáng)大需求使得現(xiàn)代集成電路系統(tǒng)的規(guī)模和復(fù)雜度日益提高。在系統(tǒng)芯片(SOC)設(shè)計(jì)中，可以利用IP構(gòu)成復(fù)雜的大規(guī)模系統(tǒng)。但是，SOC的驗(yàn)證已成為設(shè)計(jì)流程中工作量最大的工作。我們認(rèn)為系統(tǒng)的驗(yàn)證應(yīng)當(dāng)是模擬仿真、形式化和半形式化等方法的混合驗(yàn)證過程?；跀嘌缘尿?yàn)證(ABV)是把形式化方法集成到傳統(tǒng)模擬流程中的一種有效的方法。在RTL設(shè)計(jì)中插入設(shè)計(jì)意圖(斷言)，通過模擬或形式化技術(shù)來檢查該設(shè)計(jì)是否滿足這些斷言

2、。 本文在總結(jié)國內(nèi)外基于斷言驗(yàn)證研究成果的基礎(chǔ)上，提出了系統(tǒng)抽象后原子命題為三值的模型檢驗(yàn)技術(shù).研究了基于PSL的動態(tài)和靜態(tài)驗(yàn)證方法。主要內(nèi)容包括： 解決了基于三值邏輯的模型檢驗(yàn)問題。在模型檢驗(yàn)中，狀態(tài)爆炸是影響其應(yīng)用的關(guān)鍵。本文的解決方案是對系統(tǒng)進(jìn)行抽象，以減少其狀態(tài)空間。系統(tǒng)模型采用不完全的Kripke結(jié)構(gòu)表示，在此結(jié)構(gòu)下，定義了三值CTL邏輯公式的形式化語義，并用此邏輯公式表示系統(tǒng)的性質(zhì)。提出了基于不完全的krip

3、ke結(jié)構(gòu)的三值邏輯模型檢驗(yàn)算法，并給出了一個(gè)證明系統(tǒng)，在屬性驗(yàn)證是未知情況時(shí)，從該證明系統(tǒng)中可推導(dǎo)出正例或反例，為系統(tǒng)能夠進(jìn)一步驗(yàn)證提供參考信息。同時(shí)，為了使該模型檢驗(yàn)具有更廣泛的應(yīng)用，還提出了將模態(tài)轉(zhuǎn)移系統(tǒng)轉(zhuǎn)換成不完全的Kripke結(jié)構(gòu)的方法，通過該轉(zhuǎn)換再利用上述算法能夠?qū)崿F(xiàn)基于模態(tài)轉(zhuǎn)移系統(tǒng)的三值邏輯模型檢驗(yàn)。 提出了在模型檢驗(yàn)中空屬性問題的探測方法。一個(gè)公式描述了系統(tǒng)所具有的屬性，若公式中的一個(gè)子公式的真值對該公式的真值不會