抽取謂詞以改進性質導向可達性技術

Improving Property Directed Reachability by Predicate Extraction

江俊毅(Chun-Yi Chiang)

指導教授 ： 黃鐘揚

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2020年)

https://doi.org/10.6342/NTU202001451

摘要

自從在2011年被提出後，性質導向可達性技術至今仍是最好的模型檢查演算法。但是仍有許多的案例是性質導向可達性技術難以解決的，因此，為了改進這個演算法，有許多的研究先後被發表。在這篇論文中，我們藉由獨立的檢查謂詞以輔助性質導向可達性演算法。此外，作為證明的例子，我們也提供了兩種能夠輕易從演算過程中得出的樣式。原本的性質導向可達性演算法與新方法皆被實作於Ia2b這個自製的模型檢查環境上。透過利用硬體模型檢查比賽的資料所做的實驗得知，我們所提出的方法能夠解出比原本的性質導向可達性技術更多的案例。

關鍵字

正規驗證 ； 模型檢查 ； 可滿足性問題 ； 性質導向可達性技術 ； 謂詞修正

並列摘要

Since proposed in 2011, PDR (IC3) has been the best model checking algorithm until now. However, there are still many cases that PDR struggles to solve. Hence, many works are presented to enhance the algorithm. In this thesis, we propose a general method to aid PDR by solving predicate separately. Furthermore, we provide two kinds of useful pattern easily recognized from the solving process as example. The original PDR algorithm and the new feature are implemented on a custom model checking environment called Ia2b. The experiment on HWMCC benchmarks shows that our method can solve more cases than the classic PDR.

並列關鍵字

Formal Verification ； Model Checking ； Satisfiability Problem ； Property Directed Reachability ； Predicate Refinement

參考文獻

Randal E Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 100(8):677–691, 1986.

João P Marques-Silva and Karem A Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506–521, 1999.

Hantao Zhang. Sato: An efficient propositional prover. In International Conference on Automated Deduction, pages 272–275. Springer, 1997.

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, 2001.

E Goldberg and Y Novikov. Berkmin: A fast and robust sat-solver. In Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition, pages 142–149. IEEE, 2002.