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

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

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

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

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