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

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

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

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

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