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

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

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

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

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