基于永真式判定算法的控制器綜合驗(yàn)證方法的研究.pdf

1、目前隨著系統(tǒng)復(fù)雜度的增大和電子設(shè)計(jì)自動(dòng)化技術(shù)的提高,驗(yàn)證過(guò)程在整個(gè)集成電路系統(tǒng)設(shè)計(jì)中所占的份量也越來(lái)越大,驗(yàn)證工作需要大量的人力資源和財(cái)力資源,并逐漸演變成設(shè)計(jì)工作的瓶頸,因?yàn)槿魏我环NEDA工具都不能完全確保系統(tǒng)設(shè)計(jì)的正確性。隨著半導(dǎo)體制造工藝水平的快速發(fā)展、以及系統(tǒng)規(guī)模的不斷增大,使得傳統(tǒng)的驗(yàn)證工具無(wú)法勝任目前系統(tǒng)設(shè)計(jì)正確性的驗(yàn)證任務(wù)。
　　系統(tǒng)設(shè)計(jì)者常常面臨著一系列巨大壓力,設(shè)計(jì)不僅要達(dá)到較高的集成度,同時(shí)還要考慮面向市場(chǎng)的時(shí)

2、間,所以系統(tǒng)設(shè)計(jì)者面臨著功能完全準(zhǔn)確和推向市場(chǎng)時(shí)間的雙重壓力。當(dāng)前復(fù)雜的專用集成電路和IC芯片設(shè)計(jì)中的驗(yàn)證工作占用了整個(gè)設(shè)計(jì)過(guò)程的百分之七十甚至更多,驗(yàn)證工程師和設(shè)計(jì)工程師的比例約達(dá)到三比一才能確保系統(tǒng)設(shè)計(jì)順利地進(jìn)行。通常設(shè)計(jì)過(guò)程中的錯(cuò)誤越早被發(fā)現(xiàn),修改錯(cuò)誤的代價(jià)將得到減低并且由錯(cuò)誤帶來(lái)的損失也將得到減小,所以對(duì)驗(yàn)證方法的研究勢(shì)在必行?！白疃痰尿?yàn)證時(shí)間,最完備的驗(yàn)證結(jié)果”是目前系統(tǒng)設(shè)計(jì)正確性驗(yàn)證中的重點(diǎn)追求目標(biāo)。
　　綜合就是由E

3、DA設(shè)計(jì)工具自動(dòng)完成系統(tǒng)設(shè)計(jì)的過(guò)程。數(shù)字系統(tǒng)常常包括數(shù)據(jù)處理器和控制器兩大基本部件,相應(yīng)地便有處理器綜合和控制器綜合,本論文主要研究控制器綜合結(jié)果的正確性驗(yàn)證。所謂控制器綜合技術(shù)是指經(jīng)過(guò)一系列的優(yōu)化和化簡(jiǎn)等手段,在實(shí)現(xiàn)預(yù)期功能的前提下,使得控制器芯片性能達(dá)到最優(yōu)。論文采用有限狀態(tài)機(jī)系統(tǒng)描述控制器綜合前的規(guī)范行為,用電路網(wǎng)表表示控制器綜合結(jié)果的結(jié)構(gòu)實(shí)現(xiàn)。在較為深入、全面地研究控制器綜合特點(diǎn)的基礎(chǔ)上,采用狀態(tài)轉(zhuǎn)換圖描STG_ORG與STG_

4、EXT述控制器綜合前后的行為功能,用三元組V=(Q,Y(X,Q),F(X,Q))表示圖中的頂點(diǎn),Q為狀態(tài)標(biāo)識(shí),Y(X,Q)為控制輸出函數(shù),F(X,Q)為狀態(tài)轉(zhuǎn)換函數(shù),論文采用多維體陣列表示Y和F,為了判斷兩多維體的等價(jià)性,論文引入了多維體同或運(yùn)算符,采用基于同或運(yùn)算符的永真式判定算法驗(yàn)證相應(yīng)頂點(diǎn)對(duì)的等價(jià)性。
　　論文用多維體邏輯函數(shù)描述狀態(tài)轉(zhuǎn)換圖各個(gè)頂點(diǎn)的控制輸出和狀態(tài)轉(zhuǎn)換條件,采用便于計(jì)算機(jī)內(nèi)部表示的多維體陣列描述多維體邏輯函數(shù)

5、;然后利用永真式判定算法判斷當(dāng)前頂點(diǎn)對(duì)的控制輸出函數(shù)是否一致;若一致,再利用論文定義的多維體同或運(yùn)算符求出當(dāng)前頂點(diǎn)對(duì)的所有下一頂點(diǎn)對(duì),遞歸地采用永真式判定算法匹配當(dāng)前頂點(diǎn)對(duì)的所有下一頂點(diǎn)對(duì)。基于永真式判定算法的驗(yàn)證方法適于高抽象層次、高復(fù)雜度、高集成度系統(tǒng)設(shè)計(jì)的正確性驗(yàn)證。
　　論文第五章給出一個(gè)簡(jiǎn)單飲料控制器的規(guī)范描述,然后在Quartus II環(huán)境下,用VHDL語(yǔ)言實(shí)現(xiàn)該飲料控制器,并對(duì)設(shè)計(jì)結(jié)果進(jìn)行了模擬驗(yàn)證;任意給定兩個(gè)狀態(tài)