請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/53652
標題: | 利用邏輯閘層級抽象化技術增進性質導向可達性技術 Improving Property Directed Reachability Using Gate-Level Abstraction |
作者: | Kuan Fan 范寬 |
指導教授: | 黃鐘揚 |
關鍵字: | 性質導向可達性技術,邏輯閘層級抽象化技術, Property Directed Reachability,Gate-Level Abstraction, |
出版年 : | 2015 |
學位: | 碩士 |
摘要: | 性質導向可達性技術是一種高效的模型驗證演算法。然而,對於大規模集成電路的驗證,設計邏輯的複雜性可能會阻礙性質導向可達性技術建構可達性之抽象,導致未能成功證明。在本篇論文中,我們提出了整合性質導向可達性技術與邏輯閘級,混合抽象技術,這使得性質導向可達性技術成為更具擴展性的模型驗證方法。我們將此技術實作於ABC且評估其效能於HWMCC13,HWMCC14。我們的實驗結果顯示,該方法顯著優於典型的性質導向可達性技術且與其有可觀的互補性。 Property directed reachability(PDR aka IC3) is an efficient and complete model checking procedure. However, for large problems, the complexities of design logic might hinder PDR from construction of over-approximations, leading to failure to prove them. In this thesis, we present a novel model-checking technique that integrates PDR/IC3 with gate-level, hybrid abstraction, which makes PDR a more scalable model checking method. We implemented the technique in ABC and evaluated it on the HWMCC13, HWMCC14 benchmark suites. Our results show that the proposed method significantly outperforms standard PDR and complements it on a large number of benchmark instances. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/53652 |
全文授權: | 有償授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-104-1.pdf 目前未授權公開取用 | 2.58 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。