利用動態時間框架延展增進性質導向可達性技術

Improving Property Directed Reachability Using Dynamic Timeframe Expansion

楊承翰(Cheng-Han Yang)

指導教授 ： 黃鐘揚

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

https://doi.org/10.6342/NTU201702869

摘要

性質導向可達性技術自從在2011年被發表之後，一直是最有效率的模型驗證演算法。不像其他的演算法往往只偏向於安全或不安全的案例其中一者，性質導向可達性技術對於兩者都能有不錯的效能。然而，仍然有些案例是難以被解決的，所以一直有對於如何改進性質導向可達性技術的研究。在這篇論文中，我們提出了兩種將有界模型驗證融合進性質導向可達性技術的方法，以及一種結合原本的性質導向可達性技術和以上兩種演算法的混合演算法。我們在V3的框架上實做了我們的演算法，並用硬體模型驗證競賽的案例進行測試。實驗結果指出我們的演算法可以在較短的時間內解出比原本的演算法還多的案例。

關鍵字

正規驗證 ； 模型檢查 ； 可滿足性問題 ； 性質導向可達性技術 ； 時間框架延展

並列摘要

Property Directed Reachability (PDR) has been the most efficient model checking algorithm since its publication in 2011. Unlike other algorithms which often prefers either SAT cases (bug finders) or UNSAT cases (prover), PDR is well balanced that it can solve both categories efficiently. However, there are still some hard cases that PDR fails to solve, so researchers keep finding ways to improve PDR. In this thesis, we propose two modifications that integrate the idea of bounded model checking (BMC) into PDR, and a hybrid version that combines those two methods with original PDR. We implement the algorithms on V3 framework and test the performance using HWMCC benchmarks. Experiment shows that our algorithm can solve more cases than the original PDR algorithm with less average runtime.

並列關鍵字

Formal Verification ； Model Checking ； Satisfiability Problem ； Property Directed Reachability ； Timeframe Expansion

參考文獻

[1] K. L. McMillan, Symbolic model checking. Springer US, 1993.

[2] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: Engineering an Efficient SAT Solver. DAC, 2001.

[3] M. Sheeran, S. Singh, and G. Stålmarck, Checking safety properties using induction and a SAT-solver. FMCAD, 2000.

[6] A. R. Bradley, SAT-based model checking without unrolling. VMCAI, 2011.

[7] Hardware Model Checking contest. http://fmv.jku.at/hwmcc15/.