soc設(shè)計(jì)中驗(yàn)證方法的研究

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

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

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

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

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

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

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

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

8、placethemaindeviceofwholesystem．Inordertoensurethedesignofdeviceiscorrectandshortenthedevelopmentcyclefordesigning,theverificationtodesignresultbecomemoreandmoreimportant．SimulationiSnecessarytothedesi