利用時態分解技術增進性質導向可達性技術

Improving Property Directed Reachability with Temporal Decomposition

楊明仁(Ming-Jen Yang)

指導教授 ： 黃鐘揚

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

https://doi.org/10.6342/NTU201601674

摘要

因為對於安全或是不安全的案例都有突出的效能，性質導向可達性技術從二零一一年發表以來一直是模式驗證問題中最有效率的演算法。然而，因為模式驗證問題本質上的高複雜度，還是有許多的案例沒有被驗證。因此，改善性質導向可達性技術的研究是一個非常重要的主題，近來也產生了許多相關的研究。在這篇論文中，我們提出了三種基於將時態分解技術的概念融合於性質導向可達性技術的創新方法。我們將我們所提出的方法實作於“驗證三”的驗證架構中，並且使用世界”硬體模式驗證競賽”的案例與原本的性質導向可達性技術做比較。實驗結果顯示我們的方法可以驗證許多原本未被驗證的案例，對不安全的案例有一點四倍的運作時間提升，代表著這些方法可以與原本的性質導向可達性技術在相當多的基準點上互補。

關鍵字

驗證 ； 正規驗證 ； 性質導向可達性 ； 時態分解

並列摘要

Property Directed Reachability has always been the most efficient algorithm for the safety property checking problem for its well performance on both safe and unsafe case since its publication in 2011. However, there are still a large number of cases remaining unsolved due to the intrinsic high complexity of model checking problem. Therefore, improving PDR is an important subject and attracts lots of research recently. In this paper, we present three novel approaches that integrate a sequential optimization technique, called temporal decomposition into PDR. We implemented our work in V3 and compared to original PDR in V3 on HWMCC benchmarks. The experimental result shows that the proposed methods solved many originally unsolved cases, and improved unsafe cases by 1.4x in runtimes. It means that these methods can complement original PDR on a large set of benchmarks.

並列關鍵字

Verification ； Formal Verification ； PDR ； Temporal Decomposition

參考文獻

[2] McMillan, Kenneth L. "Symbolic model checking." Symbolic Model Checking. Springer US, 1993. 25-60.

[4] McMillan, Kenneth L. "Interpolation and SAT-based model checking. "International Conference on Computer Aided Verification. Springer Berlin Heidelberg, 2003.

[8] Cheng-Yin Wu and Chung-Yang (Ric) Huang. “V3: An extensible framework for hardware verification”, https://github.com/chengyinwu/V3.

[9] Hardware model checking competition. http://fmv.jku.at/hwmcc/.

[14] Backes, John D., and Marc D. Riedel. "Using cubes of non-state variables with property directed reachability." Proceedings of the Conference on Design, Automation and Test in Europe. EDA Consortium, 2013.