A comparison of BDDs, BMC, and sequential SAT for model checking

被引：2

作者：

Parthasarathy, G ^{[1
]}

Iyer, MK ^{[1
]}

Cheng, KT ^{[1
]}

Wang, LC ^{[1
]}

机构：

[1] Univ Calif Santa Barbara, Santa Barbara, CA 93106 USA

来源：

EIGHTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS | 2003年

关键词：

D O I：

10.1109/HLDVT.2003.1252490

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

BDD-based model checking and bounded model checking (BMC) are the main techniques currently used in formal verification. An approach to unbounded model checking based on a sequential SAT solver was described in [8]. In general, there are robustness issues in SAT-based versus BDD-based model checking. The research reported in this paper attempts to analyze the asymptotic run-time behavior of modem BDD-based and SAT-based techniques for model checking to determine the circuit characteristics which lead to worst-case behavior in these approaches. We show evidence for a run-time characterization based on sequential correlation and clause density. We demonstrate that it is possible to predict the worst-case behavior of BMC based on these characterizations. This leads to some interesting insights into the behavior of these techniques on a variety of example circuits.

引用

页码：157 / 162

页数：6

共 50 条

[1] Can BDDs compete with SAT solvers on bounded model checking?
Cabodi, G
Camurati, P
Quer, S
[J]. 39TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2002, 2002, : 117 - 122
[2] Learning from BDDs in SAT-based bounded model checking
Gupta, A
Ganai, M
Chao, W
Yang, ZJ
Ashar, P
[J]. 40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 824 - 829
[3] On the relation between SAT and BDDs for equivalence checking
Reda, S
Drechsler, R
Orailoglu, A
[J]. PROCEEDING OF THE 2002 3RD INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN, 2002, : 394 - 399
[4] Abstraction and BDDs complement SAT-based BMC in DiVer
Gupta, A
Ganai, M
Wang, C
Yang, ZJ
Ashar, P
[J]. COMPUTER AIDED VERIFICATION, 2003, 2725 : 206 - 209
[5] Equivalence checking combining a structural SAT-solver, BDDs, and simulation
Paruthi, V
Kuehlmann, A
[J]. 2000 IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN: VLSI IN COMPUTERS & PROCESSORS, PROCEEDINGS, 2000, : 459 - 464
[6] Symbolic Model Checking without BDDs
Biere, A
Cimatti, A
Clarke, E
Zhu, YS
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1999, 1579 : 193 - 207
[7] Safety property verification using sequential SAT and bounded model checking
Parthasarathy, G
Iyer, MK
Cheng, KT
Wang, LC
[J]. IEEE DESIGN & TEST OF COMPUTERS, 2004, 21 (02): : 132 - 143
[8] GENERATING BDDS FOR SYMBOLIC MODEL CHECKING IN CCS
ENDERS, R
FILKORN, T
TAUBNER, D
[J]. DISTRIBUTED COMPUTING, 1993, 6 (03) : 155 - 164
[9] Efficient reachability checking using sequential SAT
Parthasarathy, G
Iyer, MK
Cheng, KT
Wang, LC
[J]. ASP-DAC 2004: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2004, : 418 - 423
[10] GENERATING BDDS FOR SYMBOLIC MODEL CHECKING IN CCS
ENDERS, R
FILKORN, T
TAUBNER, D
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 575 : 203 - 213

← 1 2 3 4 5 →