模型檢驗器前端系統(tǒng)的設(shè)計與實現(xiàn).pdf

1、設(shè)計大規(guī)模的復(fù)雜的數(shù)字系統(tǒng)中關(guān)鍵問題之一是如何檢查設(shè)計的正確性。但是，傳統(tǒng)的驗證技術(shù)例如模擬、仿真和測試，只能針對某些典型的情況或隨機進行，這就難以完全排除所有設(shè)計錯誤。傳統(tǒng)的驗證技術(shù)已經(jīng)無法適應(yīng)目前集成電路芯片技術(shù)高速發(fā)展的需求。
　　本論文就是針對上述問題，研究一種新的驗證技術(shù)－模型檢驗。模型檢驗的基本思想是用分支時態(tài)邏輯公式 f表達系統(tǒng)（程序或電路）的所期望的性質(zhì)，用有限狀態(tài)機（Kripke結(jié)構(gòu)）M={S，R，L}表示系統(tǒng)的

2、狀態(tài)轉(zhuǎn)移結(jié)構(gòu)，通過遍歷有限狀態(tài)機來檢驗時態(tài)邏輯公式的正確性 f:{s∈S|M，s|=f}。如不能驗證公式 f的正確性，系統(tǒng)將給出一個反例，使用戶發(fā)現(xiàn)公式不成立的原因。
　　模型檢驗不能直接對硬件電路設(shè)計描述文件（如Verilog程序）進行驗證，必須將硬件電路設(shè)計描述文件轉(zhuǎn)換為有限狀態(tài)機。本論文就是為了解決這個問題，研究模型檢驗器的前端系統(tǒng)，即如何從硬件描述語言Verilog提取有限狀態(tài)機。
　　主要的工作是開發(fā)了兩個軟件編譯

3、器：VL2BLIF編譯器和BLIF2FSM編譯器。VL2BLIF編譯器的核心功能是把Verilog程序編譯為BLIF-MV程序。BLIF2FSM編譯器的核心功能是從BLIF-MV程序中提取出有限狀態(tài)機，并使用二叉判定圖表示有限狀態(tài)機。主要工作內(nèi)容為：
　　1.編寫lex與yacc源程序，使編譯器能夠自動地分析Verilog程序與BLIF-MV程序的詞法、語法、語義。生成編譯器可處理的中間數(shù)據(jù)結(jié)構(gòu)，并自動檢查Verilog程序與BL

4、IF-MV程序的靜態(tài)語義錯誤。
　　2．詳細研究 Verilog程序中的各種語句如何描述數(shù)字電路的狀態(tài)轉(zhuǎn)換關(guān)系。并研究在BLIF-MV程序中如何使用時間機和非時間機來描述狀態(tài)轉(zhuǎn)換關(guān)系和更新狀態(tài)變量。重點分析含有延遲與事件控制的過程賦值語句如何轉(zhuǎn)變?yōu)闀r間機。
　　3．研究如何使用布爾函數(shù)來描述 BLIF-MV語言的狀態(tài)轉(zhuǎn)換關(guān)系和多值變量的關(guān)系。
　　4．研究二叉判定圖表示布爾函數(shù)的方法。并分析二叉判定圖減小存儲空間的方法