- 學位論文
利用高階設計資訊以增進電路之安全性屬性檢定效能
Improving Safety Property Checking by High-Level Design Information
摘要
安全性屬性檢定在設計驗證之中是相當重要的技術。這項技術確保預期設計的正確性，或者當設計中的安全性屬性被違反時，能夠提供反例以供設計者偵錯。 在過去的研究當中，安全性屬性檢定在可滿足性解法器(SAT solver)的應用下解地不錯。由於要使用可滿足性解法器，問題本身會被翻譯至位元階層的邏輯式子，以便使用位元階層的邏輯操作如：化簡合取範式(CNF)和抽象並完善技術。但是這問題原本就來自暫存器轉移階層(RTL)設計。在暫存器轉移設計階層中，有許多高階設計資訊可能對安全性屬性檢定有幫助，例如有限狀態機(FSM)和字級表示式。在這篇論文中，字級表示式用來化簡邏輯表示式，從有限狀態機的資訊中抽取路徑限制用來幫助可滿足性解法器。我們的實驗顯現出我們的結果與另一個優秀的安全性檢定器ABC相當接近。部分測資在路徑限制的幫助下甚至能贏過ABC。因此高階設計資訊的確在安全性屬性檢定效能上有很好的提升效果。
並列摘要
Safety property checking is an important technique in design verification. It ensures the correctness of the expected design behavior, or, when the property is falsified, provides a counter example for debugging. In recent years, the problem is solved well with the help of SAT solver. Due to the nature of SAT solver, the problem input is translated into a bit-level logic formula and focused on the operation of bit-level logic like CNF minimization and abstraction and refinement technique. However, the problem is originally described in the RTL design. The high level design information such as Finite State Machine (FSM) and word-level expression might be helpful for the safety property checking problem. In this thesis, the word-level expression is used to reduce the logic representation, and the information provided by FSM is used to guide the SAT solver by path constraint. Our experimental result showed that the performance is closed to one of the safety property checker ABC. The performance with path constraint even wins the ABC. Thus, the high level design information does have a good effect on safety property checking.