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

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

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

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

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

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