基于GSTE模型檢測的信號并串轉(zhuǎn)換模塊功能驗證的研究.pdf

1、隨著集成電路設(shè)計的發(fā)展和不斷更新?lián)Q代,電路設(shè)計周期縮短,使得芯片的驗證愈加重要。同時與日俱增的電路復(fù)雜程度也使得驗證愈加困難。傳統(tǒng)的芯片驗證方法是基于模擬仿真的方式,通過測試用例,觀察在給定的輸入下是否能得到期望的輸出。這種方法驗證周期長且覆蓋率有限。形式化驗證是一種基于數(shù)學(xué)推理的驗證方法。它將系統(tǒng)和其規(guī)范抽象成數(shù)學(xué)模型,通過推理得出系統(tǒng)是否滿足規(guī)范。形式化驗證方法能達(dá)到100％的覆蓋率,且能給出相關(guān)反例。但該方法由于計算復(fù)雜度的問題,

2、只適用于較小規(guī)模的電路驗證,規(guī)模增大后會帶來狀態(tài)爆炸的問題。為提高驗證效率和驗證規(guī)模,需要使用良好的數(shù)據(jù)結(jié)構(gòu)和算法驗證模型構(gòu)筑驗證系統(tǒng)。
　　本文從常用形式化驗證數(shù)據(jù)結(jié)構(gòu)和關(guān)鍵算法出發(fā),結(jié)合相關(guān)技術(shù)的對比,討論了將AIG和SAT求解器應(yīng)用到模型檢測算法GSTE中的方法,以期望提高驗證的規(guī)模和效率。同時本文對GSTE算法的理論做了若干補(bǔ)充。
　　文中首先簡要介紹了幾種常用的模型檢測方法并分析了其優(yōu)缺點,其次介紹了GSTE模型檢

3、測方法,包括它對STE的擴(kuò)展以及斷言圖等內(nèi)容,并對其理論做了一定補(bǔ)充,證明了一種縮小斷言圖存儲空間方法的正確性。通過對模型檢測常用數(shù)據(jù)結(jié)構(gòu)BDD的分析,基本找出了其驗證范圍限制的原因并確立了以AIG為主要數(shù)據(jù)結(jié)構(gòu)的策略。同時,文中使用量詞調(diào)度的方法,有效控制了驗證過程中AIG的規(guī)模,并對調(diào)度方法進(jìn)行一定改進(jìn),使調(diào)度更加快速有效。在使用AIG的同時,本文設(shè)置了若干閾值,在合適的時間使用BDD對AIG進(jìn)行化簡并在可行時,直接使用BDD繼續(xù)驗

4、證。通過和基于BDD的方法對比,使用AIG可以很大程度上減少內(nèi)存消耗,從而給提高驗證規(guī)模帶來可能。
　　針對使用AIG仍然可能存在的狀態(tài)爆炸問題,本文在AIG驗證遇到瓶頸時,結(jié)合使用SAT求解器完成驗證中關(guān)鍵的計算步驟,即量詞消除,解決了AIG狀態(tài)爆炸問題。并且文中通過使用針對SAT求解器驗證的優(yōu)化,有效地減少了量詞消除所需時間,整體上提高了驗證效率。通過與基于BDD的GSTE模型檢測方法的性能對比,證明了結(jié)合AIG和SAT求解器