自適應多時間框架的性質導向可達性演算法

Abstract

性質導向可達性(Property Directed Reachability, PDR)演算法為現今解決模型檢查(Model Checking)問題最有效之技術之一。然而，在一般典型的實現方法中，常因數量過多的回溯檢查(backtracking checks)而導致效率低落。雖然回溯檢查中大多數的證明義務(proof obligations)相對容易被阻擋，但少數困難的證明義務卻佔據了大比例的求解時間。為了解決此問題，我們提出一種多時間框架的性質導向可達性演算法，將動態時間框架擴展策略整合進多時間框架的轉移模型中，利用多時間框架電路之邏輯推論，以加速對困難證明義務之阻擋過程。 儘管這樣的整合在概念上看似簡單，先前的研究卻在正確性與完備性方面遭遇挑戰。本研究透過額外的精化機制克服這些問題，並提供形式化的正確性與完備性證明。 我們將所提出的演算法實作於兩個先進的性質導向可達性框架——ABC 與 rIC3——並以硬體模型驗證競賽(HWMCC)的基準測試集進行實驗評估。實驗結果顯示，與典型的單時間框架相比，我們的方法在效能上表現更為優異。

Property Directed Reachability (PDR) is one of the most effective techniques for solving model checking problems. However, in its typical implementation, it often suffers from excessive backtracking. While most proof obligations are relatively easy to block, a small number of difficult ones dominate the solving time. To address this inefficiency, we propose a multi-timeframe PDR algorithm that integrates a dynamic timeframe expansion strategy into a multi-timeframe transition framework. This design leverages reasoning across multiple timeframes to accelerate the blocking of difficult obligations. Although this integration appears straightforward, prior attempts have encountered challenges regarding soundness and completeness. Our approach resolves these issues through additional refinement mechanisms, supported by formal proofs of correctness and completeness. We implement the proposed algorithm on two state-of-the-art PDR frameworks—ABC and rIC3—and evaluate it using benchmarks from the Hardware Model Checking Competition (HWMCC). Experimental results show that our approach consistently outperforms typical single-timeframe PDR in both frameworks.