soc設(shè)計中驗證方法的研究

《soc設(shè)計中驗證方法的研究》由會員上傳分享，免費在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。

1、北京交通人學(xué)頌I·學(xué)位論艾北京交通大學(xué)2001級碩：j二學(xué)位論文摘要SoC設(shè)計中的驗證方法研究電子信息工程學(xué)院碩士研究生杜慧以往復(fù)雜系統(tǒng)的主要部分，在SoC技術(shù)支持下，完全由一塊集成電路芯片所代替。SoC器件的功能越來越多，器件結(jié)構(gòu)越來越復(fù)雜。為了保證器件設(shè)計的正確性，縮短器件設(shè)計開發(fā)周期，對設(shè)計結(jié)果的驗證顯得越來越重要。不管是功能級、邏輯級還是門級，仿真驗證是一個電路設(shè)計必不可少的。隨電路規(guī)模的增大，基于仿真向量的仿真驗證方法其復(fù)雜度也呈指數(shù)上升，仿真測試方法已經(jīng)難以滿足電路驗證的要求。現(xiàn)在，當(dāng)設(shè)計到達(dá)門級

2、或晶體管級時，仿真速度會變得很慢，從而不再適合驗證SoC設(shè)計。同時由于SoC的高度復(fù)雜性，極大的損害了模擬時的可控性和可觀察性。為解決傳統(tǒng)驗證方法的不足，在學(xué)術(shù)界的數(shù)學(xué)家和計算機科學(xué)家提出的形式化方法已經(jīng)經(jīng)歷了二十多年的發(fā)展過程。在實際應(yīng)用中，模型驗證的算法和建模的規(guī)范都集成到了特定的驗證工具中。模型驗證問題的實質(zhì)是給出一個狀態(tài)并發(fā)系統(tǒng)的Kripke結(jié)構(gòu)描述，以及該系統(tǒng)所必須要滿足的約束規(guī)范，利用驗證算法來檢驗Kripke結(jié)構(gòu)是否滿足系統(tǒng)的約束規(guī)范。但如果狀態(tài)機中存在與設(shè)計要求和設(shè)計約束條件不符合之處，這種方

3、法無法檢查出來。同時由于系統(tǒng)規(guī)模的不斷擴大，這種方法也難以全面完成驗證要求。本文對系統(tǒng)級設(shè)計結(jié)果驗證問題以及以系統(tǒng)任務(wù)為模型的任務(wù)模型檢驗方法MCTL進(jìn)行了討論。MCTL仍然以狀態(tài)集合為基礎(chǔ)，但所關(guān)心的不是共有多少狀態(tài)，以及能否從～個指定狀態(tài)到達(dá)另一個指定狀態(tài)，而是在滿足指定的約束條件下，兩個狀態(tài)組合之間是否存在指定的轉(zhuǎn)換關(guān)系。由于關(guān)心的是狀態(tài)組合之間轉(zhuǎn)換形式是否存在，這樣就不必關(guān)心一共可能具有多少種狀態(tài)及其具體形式，而把模型表示的重點和檢驗的內(nèi)容轉(zhuǎn)變?yōu)闋顟B(tài)組合之間的轉(zhuǎn)換關(guān)系是否存在上。為了實現(xiàn)系統(tǒng)級設(shè)計結(jié)果

4、檢驗，本文第三部分討論了功能、任務(wù)及其約束條件，以及任務(wù)的規(guī)范定義。根據(jù)討論的結(jié)果，本文第四部分給出了建立功能模塊、驗證規(guī)范的具體規(guī)則，提出了具體的算法結(jié)構(gòu)。本文第五部分對MCTL軟件系統(tǒng)的編制結(jié)構(gòu)及實現(xiàn)算法進(jìn)行了介紹。同時，給出了相應(yīng)的應(yīng)用實例。本文作者根據(jù)MCTL算子、約束條件和MCrL算法，編制了一個基于北京交通人學(xué)壩i。學(xué)位論文任務(wù)模型的驗證系統(tǒng)——McrL系統(tǒng)。整個系統(tǒng)可以分為用戶設(shè)計模塊輸入Designed和電路功能規(guī)范驗證Verify兩個部分。其中Designed主要針對用戶，接受用戶輸入的設(shè)計

5、模塊；而Verify主要針對驗證者，根據(jù)設(shè)計要求輸入驗證規(guī)范，并據(jù)此對用戶設(shè)計進(jìn)行驗證，同時給出驗證結(jié)果。目前大多數(shù)算法以二叉判定圖(BinaryDecisionDiagraph)為基礎(chǔ)。但是BDD卻并不適用于系統(tǒng)級驗證MCTL系統(tǒng)中，因為其所關(guān)心的不是共有多少狀態(tài)，以及能否從一個指定狀態(tài)到達(dá)另一個指定狀態(tài)，而是在滿足指定的約束條件下，兩個狀態(tài)組合之間是否存在指定的轉(zhuǎn)換關(guān)系。這樣就把模型表示的重點和檢驗的內(nèi)容轉(zhuǎn)變?yōu)闋顟B(tài)組合之間的轉(zhuǎn)換關(guān)系是否存在上。于是本文提出了一種基于圖的可供MCTL系統(tǒng)驗證的基本功能算子圖

6、?；竟δ芩阕訄D是一個無向圖，頂點可以存儲基本功能算子的信息，邊可以正確表現(xiàn)各個基本功能算子之間的連接關(guān)系，同時在驗證過程中，只要驗證設(shè)計規(guī)范基本功能算子圖是實現(xiàn)結(jié)構(gòu)基本功能算子圖的子圖，則驗證完成，可證明實現(xiàn)結(jié)構(gòu)的設(shè)計是正確的，對于驗證過程的搜索是十分便利的。本文主要對以下幾個軟件的編制思想進(jìn)行了介紹：(1)庫函數(shù)(2)自動布線功能(3)功能描述規(guī)則輸入智能化(4)基本功能算子圖的生成(5)后臺故障識別另外，本文對軟件中所設(shè)計的數(shù)據(jù)結(jié)構(gòu)和軟件的功能實現(xiàn)也進(jìn)行了詳細(xì)的介紹。在撰寫本文和程序測試的過程中，作者也

7、發(fā)現(xiàn)了軟件的一些局限性，并提出了一些改進(jìn)建議。關(guān)鍵詞：BDD，存儲結(jié)構(gòu)，任務(wù)模型，SoC，驗證北京交通人學(xué)壩{j學(xué)化論文StudyforVerificationMethodologyofSoCHulDUSchoolofElectronicsandInformationEngineeringBeijingJiaotongUniversityMasterThesis(Summary)2004．3WiththesupportoftechnologyofSoC，anintegratedcircuitehipcanre

8、placethemaindeviceofwholesystem．Inordertoensurethedesignofdeviceiscorrectandshortenthedevelopmentcyclefordesigning,theverificationtodesignresultbecomemoreandmoreimportant．SimulationiSnecessarytothedesi