不同模型檢測(cè)下信號(hào)并串轉(zhuǎn)換模塊功能建模的研究.pdf

1、傳統(tǒng)的工業(yè)電路驗(yàn)證使用的是模擬驗(yàn)證技術(shù),它的驗(yàn)證結(jié)果與其選擇的測(cè)試向量有直接關(guān)系。隨著電路規(guī)模的不斷增大,測(cè)試向量的選取難度越來(lái)越大,測(cè)試覆蓋率越來(lái)越低。近年來(lái),形式化驗(yàn)證技術(shù)逐漸成為人們研究的熱點(diǎn)。它采用數(shù)學(xué)的方法,摒棄了傳統(tǒng)的模擬驗(yàn)證中有關(guān)測(cè)試向量的部分,轉(zhuǎn)而改用規(guī)范化語(yǔ)言來(lái)描述電路的性質(zhì),再結(jié)合電路的模型和遷移關(guān)系達(dá)到驗(yàn)證的目的。它具有驗(yàn)證速度快,能夠做到全覆蓋等特點(diǎn)。但是,由于存在狀態(tài)爆炸等問(wèn)題,形式化驗(yàn)證技術(shù)的驗(yàn)證規(guī)模不是很大

2、。目前,它無(wú)法滿(mǎn)足工業(yè)上大規(guī)模集成電路的驗(yàn)證要求,只是作為學(xué)術(shù)研究出現(xiàn)在各個(gè)高校和大公司的實(shí)驗(yàn)室。
　　本文從長(zhǎng)虹公司提供的一個(gè)實(shí)際工業(yè)電路出發(fā),分別使用時(shí)序邏輯模型檢測(cè)技術(shù)和GSTE技術(shù)對(duì)其相關(guān)性質(zhì)進(jìn)行了驗(yàn)證。通過(guò)對(duì)這個(gè)實(shí)際工業(yè)電路的驗(yàn)證研究,本文旨在探究形式化驗(yàn)證技術(shù)應(yīng)用于實(shí)際工業(yè)中的可能性。
　　本文首先簡(jiǎn)單介紹了一下傳統(tǒng)的模擬驗(yàn)證技術(shù)和形式化驗(yàn)證技術(shù),并比較了兩者的優(yōu)缺點(diǎn)。然后對(duì)本文中用到的GSTE算法和時(shí)態(tài)邏輯進(jìn)行

3、了詳細(xì)的介紹,在GSTE部分,本文著重介紹了它的模型、斷言圖以及強(qiáng)滿(mǎn)足性算法等相關(guān)內(nèi)容;在時(shí)態(tài)邏輯部分,本文首先介紹了LTL的相關(guān)內(nèi)容,進(jìn)而引出對(duì)CTL相關(guān)規(guī)則的介紹,并且比較了LTL和CTL的不同和互通點(diǎn)。這部分的介紹為后文的驗(yàn)證提供了理論基礎(chǔ)。
　　在開(kāi)始驗(yàn)證前,本文首先介紹了相關(guān)的驗(yàn)證工具:VIS和 Whale,并以Counter和FIFO這兩個(gè)電路模塊為例,介紹了如何提取性質(zhì),建立CTL公式和斷言圖,以及使用驗(yàn)證工具進(jìn)行驗(yàn)