應用抽象與精細化技術增進RTL電路之安全性屬性檢定效能

Abstract

在現今的超大規模集成電路驗證問題上，特別是針對正確表達設計者意圖的屬性檢定，已經面臨了極大複雜度的議題。安全性屬性檢定是其中一個最重要的問題，是為了確保硬體系統將永遠不會走入一個設計者原先意想不到的狀態。然而在傳統上我們會在邏輯階層的布林電路上做屬性檢定，但缺點是此階層所擁有的訊息中已經失去了設計者原先的意圖。因此我們認為直接在高等抽象階層的電路上做安全性屬性檢定將會更有效率。 在這篇論文中，我們將提出一個完全以可滿足性為根基的安全性屬性檢定演算法。此演算法將直接作用於位元向量階層的暫存器轉移階層設計與屬性。我們為了更有效率的解決問題而採用了根基於抽象與精細化的技術。實驗結果已顯示出我們的方法在處理困難的屬性問題上，不論在執行時間或收斂的能力上都能夠有非常好的表現與改善。

Verification on modern VLSI designs has encountered a tremendous challenge for large design complexity issue, especially for verifying expected behavior from designer’s intent. Safety property checking is one of the most important problems to ensure that the hardware system will never fall into a state that is unexpected by designers. However, traditional assertion checking is conducted on gate-level Boolean circuits. The drawback is that the designer’s original intent is lost in this level. Therefore, it will be more efficient to perform safety property checking directly on high-level design abstraction. In this thesis, we proposed a purely SAT-based safety property checking algorithm in dealing with word-level RTL designs and properties. Our approach is based on abstraction and refinement techniques to solve the problem more efficiently. Experimental results have shown that our approach has great performance improvement in runtime and convergence ability in proving difficult properties.