電機資訊學院: 電子工程學研究所指導教授: 黃鐘揚范寬Fan, KuanKuanFan2017-03-062018-07-102017-03-062018-07-102015http://ntur.lib.ntu.edu.tw//handle/246246/276727性質導向可達性技術是一種高效的模型驗證演算法。然而，對於大規模集成電路的驗證，設計邏輯的複雜性可能會阻礙性質導向可達性技術建構可達性之抽象，導致未能成功證明。在本篇論文中，我們提出了整合性質導向可達性技術與邏輯閘級，混合抽象技術，這使得性質導向可達性技術成為更具擴展性的模型驗證方法。我們將此技術實作於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.2637857 bytesapplication/pdf論文公開時間: 2017/8/6論文使用權限: 同意有償授權(權利金給回饋本人)性質導向可達性技術邏輯閘層級抽象化技術Property Directed ReachabilityGate-Level Abstractionthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/276727/1/ntu-104-R02943084-1.pdf