一種基于斷言圖的模型抽象技術(shù)的研究.pdf

1、隨著集成電路設(shè)計(jì)復(fù)雜度的與日俱增，而芯片的更新?lián)Q代速度也在不斷加快，使得集成電路芯片的驗(yàn)證越來(lái)越困難。傳統(tǒng)的芯片驗(yàn)證主要是基于仿真模擬的驗(yàn)證，其驗(yàn)證周期長(zhǎng)，無(wú)法做到全覆蓋的用例驗(yàn)證。形式化驗(yàn)證是根據(jù)規(guī)范化語(yǔ)言描述的屬性，使用數(shù)學(xué)的方法證明其是否滿足給定的系統(tǒng)模型，具有完備性，從而避免了仿真驗(yàn)證的缺點(diǎn)。盡管如此，該方法本身就是計(jì)算復(fù)雜度敏感的，它只能驗(yàn)證較小的集成電路芯片模型，當(dāng)規(guī)模過(guò)大時(shí)，將造成狀態(tài)爆炸問(wèn)題。所以為了達(dá)到更好的性能，需要

2、采用抽象來(lái)減少用于形式驗(yàn)證所需的狀態(tài)數(shù)，與此同時(shí)需要保證抽象后的模型對(duì)于要驗(yàn)證的屬性保持與原模型具有相同的功能性，只有這樣才能保證模型抽象的正確性。
　　本文從形式化驗(yàn)證的基礎(chǔ)理論出發(fā)，對(duì)模型抽象技術(shù)和一些驗(yàn)證平臺(tái)進(jìn)行了討論，并對(duì)其應(yīng)用范圍進(jìn)行了擴(kuò)展和補(bǔ)充，以期在模型檢驗(yàn)的過(guò)程中，達(dá)到加速驗(yàn)證過(guò)程的目的。
　　文中首先介紹形式化驗(yàn)證方法、時(shí)態(tài)邏輯和模型抽象的基礎(chǔ)理論，其次介紹了 GSTE驗(yàn)證方法，并對(duì)其擴(kuò)展的部分如支持ω-r

3、egular的性質(zhì)、斷言圖等做詳細(xì)的闡述。通過(guò)對(duì) VIS平臺(tái)采用的規(guī)范化描述語(yǔ)言 CTL的詳細(xì)介紹，討論了 CTL與斷言圖的表達(dá)的范圍的關(guān)系，從而最終確立了只對(duì)不變屬性進(jìn)行對(duì)比測(cè)試。通過(guò)以上的學(xué)習(xí)和比較分析，將介紹在 VIS平臺(tái)以及在該平臺(tái)上開發(fā)的基于 GSTE驗(yàn)證方法的Whale工具，并通過(guò)引入非阻塞賦值算法解決了 VIS無(wú)法處理非阻塞賦值語(yǔ)句的缺陷，完成了對(duì) UART的寄存器傳輸級(jí)模型的 FSM的狀態(tài)轉(zhuǎn)移的驗(yàn)證和對(duì)發(fā)送的數(shù)據(jù)是否與輸

4、入數(shù)據(jù)一致的符號(hào)化驗(yàn)證。實(shí)驗(yàn)表明，該方法能夠完成測(cè)試用例的全覆蓋，說(shuō)明了該方法在實(shí)際例子中所具有的重要意義。
　　針對(duì)狀態(tài)爆炸問(wèn)題，本文將模型抽象中的模型劃分技術(shù)引入到 GSTE驗(yàn)證方法中，通過(guò)采用基于斷言圖的模型抽象技術(shù)，在對(duì)不變屬性的驗(yàn)證過(guò)程中取得了重要的性能提升。通過(guò)與 VIS中各種模型檢驗(yàn)算法的性能比較結(jié)果，證明，在引入抽象技術(shù)后，GSTE驗(yàn)證方法通過(guò)縮短到達(dá)不動(dòng)點(diǎn)的步數(shù)，使得在驗(yàn)證無(wú)反例的不變屬性例子時(shí)，具有更快的速度。