(34.201.11.222) 您好!臺灣時間:2021/02/25 13:59
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:莊世聿
研究生(外文):Shih-Yu Chuang
論文名稱:透過內插方法改善性質導向可達性技術
論文名稱(外文):Property Directed Reachability with InterpolationRefinement
指導教授:黃鐘揚
指導教授(外文):Chung-Yang Huang
口試委員:李建模許智仁
口試日期:2019-07-26
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:電機工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2019
畢業學年度:107
語文別:英文
論文頁數:44
中文關鍵詞:正規驗證模型檢查可滿足性問題性質導向可達性技術基於內插法的模型檢查演算法
DOI:10.6342/NTU201901860
相關次數:
  • 被引用被引用:0
  • 點閱點閱:27
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
自從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.
誌謝 i
中文摘要 ii
Abstract iii
Contents iv
List of Figures vi
List of Tables vii
1 Introduction 1
1.1 Related Works 2
1.2 Contributions of the Thesis 3
1.3 Organizations of the Thesis 3
2 Preliminaries 4
2.1 Propositional Satisfiability 4
2.2 Finite State Transition System 4
2.3 Model Checking Problem 5
2.4 Bounded Model Checking 6
2.5 Interpolation Based Model Checking 8
2.6 Property Directed Reachability 12
3 PDR with Interpolant Refinement 15
3.1 Motivation 15
3.2 Implementation 19
3.2.1 Blocking Phase 21
3.2.2 Refining Phase 23
3.2.3 Propagating Phase 24
3.3 Correctness 26
4 Case Study 27
4.1 Strenght and Weakness 27
4.2 Cases We Gain 28
4.3 Cases We Lose 32
5 Experimental Results 33
6 Conclusion and Future Work 42
Reference 43
[1] Kenneth L McMillan. Symbolic model checking. Springer, 1993.
[2] Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference, pages 530–535. ACM, 2001.
[3] Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. Checking safety properties using induction and a sat­solver. In International conference on formal methods in computer­aided design, pages 127–144. Springer, 2000.
[4] Kenneth L McMillan. Interpolation and sat­based model checking. In International Conference on Computer Aided Verification, pages 1–13. Springer, 2003.
[5] Armin Biere, Alessandro Cimatti, Edmund M Clarke, Ofer Strichman, Yunshan Zhu, et al. Bounded model checking. Advances in computers, 58(11):117–148, 2003.
[6] Aaron R Bradley. Sat­based model checking without unrolling. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 70– 87. Springer, 2011.
[7] Niklas Een, Alan Mishchenko, and Robert Brayton. Efficient implementation of property directed reachability. In Proceedings of the International Conference on Formal Methods in Computer­Aided Design, pages 125–134. FMCAD Inc, 2011.
[8] Robert Brayton and Alan Mishchenko. Abc: An academic industrial­strength verification tool. In International Conference on Computer Aided Verification, pages 24–40. Springer, 2010.
[9] Cheng-­Yin Wu and Chuang-­Yang(Ric) Huang. V3: An extensible framework for hardware verification. https://github.com/chengyinwe/V3.
[10] Hong­-Syun Jiang and Chung-­Yang(Ric) Huang. Enhancing property directed reachability technique through cube analysis. Master Thesis, 2015.
[11] Kuan Fan, Ming­-Jen Yang, and Chung­-Yang Huang. Automatic abstraction refinement of tr for pdr. In 2016 21st Asia and South Pacific Design Automation Conference (ASP­DAC), pages 121–126. IEEE, 2016.
[12] Ming­-Jen Yang and Chung-­Yang(Ric) Huang. Improving property directed reachability with temporal decomposition. Master Thesis, 2016.
[13] Cheng-­Han Yang and Chung-­Yang(Ric) Huang. Improving property directed reachability using dynamic timeframe expansion. Master Thesis, 2017.
[14] Yakir Vizel and Arie Gurfinkel. Interpolating property directed reachability. In International Conference on Computer Aided Verification, pages 260–276. Springer, 2014.
[15] Hardware model checking competition. http://fmv.jku.at/hwmcc17/.
[16] William Craig. Three uses of the herbrand­gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic, 22(3):269–285, 1957.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
系統版面圖檔 系統版面圖檔