Please use this identifier to cite or link to this item:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/74303
Title: | 透過內插方法改善性質導向可達性技術 Property Directed Reachability with Interpolation Refinement |
Authors: | Shih-Yu Chuang 莊世聿 |
Advisor: | 黃鐘揚(Chung-Yang Huang) |
Keyword: | 正規驗證,模型檢查,可滿足性問題,性質導向可達性技術,基於內插法的模型檢查演算法, Formal Verification,Model Checking,Satisfiability Problem,Property Directed Reachability,Interpolation Based Model Checking, |
Publication Year : | 2019 |
Degree: | 碩士 |
Abstract: | 自從2011年被提出以後,性質導向可達性演算法已經被公認為目前最佳的模型檢查引擎。然而目前還有許多案例為性質導向可達性演算法無法解決,因此改良性質導向可達性演算法一直都是個重要的問題。在這篇論文中,我們將性質導向可達性演算法與麥克米倫內插法結合使其可以跳過遞迴封鎖方塊階段所花費的巨量時間藉此改善效能。實驗結果顯示我們方法之效能在世界硬體模型檢查比賽中可以解決比性質導向可達性演算法與麥克米倫內插法更多的案例。 Property directed reachability / IC3 (PDR) has been recognized to be the most powerful model checking engine since it was proposed in 2011. However, there are still a lot of benchmarks which cannot be solved by PDR. The demand of improving PDR is quite urgent. In this thesis, we proposed a method combining PDR with McMillan's interpolant to help PDR skip the huge runtime during recursive blocking cube phase to improve the performance. The experimental result shows that our method can solve more cases than the original PDR and McMillan's interpolation-based model checker on HWMCC's benchmarks. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/74303 |
DOI: | 10.6342/NTU201901860 |
Fulltext Rights: | 有償授權 |
Appears in Collections: | 電機工程學系 |
Files in This Item:
File | Size | Format | |
---|---|---|---|
ntu-108-1.pdf Restricted Access | 2.53 MB | Adobe PDF |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.