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

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

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