請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/42444
標題: | 利用高階設計資訊以增進電路之安全性屬性檢定效能 Improving Safety Property Checking by High-Level Design Information |
作者: | Jhen-Cheng Ye 葉鎮丞 |
指導教授: | 黃鐘揚 |
關鍵字: | 安全性屬性檢定,高階設計資訊,字級表示式,有限狀態機, safety property checking,high level design information,word-level expression,Finite State Machine(FSM), |
出版年 : | 2009 |
學位: | 碩士 |
摘要: | 安全性屬性檢定在設計驗證之中是相當重要的技術。這項技術確保預期設計的正確性,或者當設計中的安全性屬性被違反時,能夠提供反例以供設計者偵錯。 在過去的研究當中,安全性屬性檢定在可滿足性解法器(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. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/42444 |
全文授權: | 有償授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-98-1.pdf 目前未授權公開取用 | 461.23 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。