Bounded Model Checking Combining Symbolic Trajectory Evaluation Abstraction with Hybrid Three-Valued SAT Solving
Bounded Model Checking Combining Symbolic Trajectory Evaluation Abstraction with Hybrid Three-Valued SAT Solving
复制标题
结合符号轨迹评估抽象与混合三值 SAT 求解的有界模型检查
DOI：
10.1007/978-3-540-72863-4_31
复制
发表时间：
2006-05
期刊：
影响因子：
--
通讯作者：
Weimin Wu
中科院分区：
文献类型：
--
作者：
Jinian Bian;Shujun Deng;Weimin Wu
基于SAT的有界模型检测（BMC）是对基于BDD的符号模型检测的一种补充技术，它有助于发现最小长度的反例。然而，对于大型真实的世界系统的模型检测，BMC仍然受到状态爆炸问题的限制，因此抽象是必要的。在本文中，BMC实现了一个更高的抽象级别-寄存器传输级（RTL）的抽象框架内的符号轨迹评估和混合三值SAT求解。提出了一种有效的RTL电路SAT求解器，并将其修改为三值求解器，用于协同BMC应用。实验结果表明，与普通BMC相比，我们的方法是有效的。
Bounded Model Checking (BMC) based on SAT is a complementary technique to BDD-based Symbolic Model Checking, and it is useful for finding counterexamples of minimum length. However, for model checking of large real world systems, BMC is still limited by the state explosion problem, thus abstraction is essential. In this paper, BMC is implemented on a higher abstraction level – Register Transfer Level (RTL) within an abstraction framework of symbolic trajectory evaluation and hybrid three-valued SAT solving. An efficient SAT solver for RTL circuits is presented, and it is modified into a three-valued solver for the cooperative BMC application. The experimental results comparing with the ordinary BMC without abstraction show the efficiency of our method.
登录
查看更多内容
DOI：
10.1109/tcad.2004.841068
发表时间：
2005-01
影响因子：
2.9
作者：
Hyeong-Ju Kang;I. Park
通讯作者：
Hyeong-Ju Kang;I. Park
DOI：
10.1007/3-540-48153-2
发表时间：
2003
期刊：
--
影响因子：
--
作者：
G. Milne;L. Pierre
通讯作者：
G. Milne;L. Pierre
DOI：
10.1016/b978-044450813-3/50026-6
发表时间：
2001
期刊：
--
影响因子：
--
作者：
E. Clarke;Holger Schlingloff
通讯作者：
E. Clarke;Holger Schlingloff
DOI：
10.1007/978-3-642-61455-2_16
发表时间：
1996-09
期刊：
--
影响因子：
--
作者：
Edmund M. Clarke;O. Grumberg;D. E. Long
通讯作者：
Edmund M. Clarke;O. Grumberg;D. E. Long
DOI：
10.1007/b93958
发表时间：
2003
期刊：
--
影响因子：
--
作者：
J. Leeuwen;D. Geist;E. Tronci;J. Leeuwen
通讯作者：
J. Leeuwen;D. Geist;E. Tronci;J. Leeuwen