SAT-based unbounded symbolic model checking
SAT-based unbounded symbolic model checking
复制标题
DOI：
10.1109/tcad.2004.841068
复制
发表时间：
2005-01
影响因子：
2.9
通讯作者：
Hyeong-Ju Kang;I. Park
中科院分区：
文献类型：
--
作者：
Hyeong-Ju Kang;I. Park
提出了一种基于布尔可满足性检验的无界符号模型检验算法。合取范式用于表示状态集和转移关系。对状态集的逻辑运算被实现为对合取范式公式的运算。提出了一个全满足过程来计算获得原像和不动点所需的存在量化。建议的satisfy-all过程是通过修改一个SAT过程，以产生所有令人满意的分配的输入公式，这是基于新的有效的技术，如行调整，使分配覆盖更多的搜索空间，排除子句管理，和两个层次的逻辑最小化，以压缩一组找到的分配。此外，在满足全部过程中引入了缓存表。对于一个满足全部的过程来说，检测先前的结果是否可以被重用是一个困难的问题。本文表明，这种情况下，可以通过比较未确定的变量和条款的集合来检测。实验结果表明，该算法比基于二叉判决树和已有的基于SAT的模型检测算法能检测更多的电路。
This paper describes a Boolean satisfiability checking (SAT)-based unbounded symbolic model-checking algorithm. The conjunctive normal form is used to represent sets of states and transition relation. A logical operation on state sets is implemented as an operation on conjunctive normal form formulas. A satisfy-all procedure is proposed to compute the existential quantification required in obtaining the preimage and fix point. The proposed satisfy-all procedure is implemented by modifying a SAT procedure to generate all the satisfying assignments of the input formula, which is based on new efficient techniques such as line justification to make an assignment covering more search space, excluding clause management, and two-level logic minimization to compress the set of found assignments. In addition, a cache table is introduced into the satisfy-all procedure. It is a difficult problem for a satisfy-all procedure to detect the case that a previous result can be reused. This paper shows that the case can be detected by comparing sets of undetermined variables and clauses. Experimental results show that the proposed algorithm can check more circuits than binary decision diagram-based and previous SAT-based model-checking algorithms.