On SAT-based bounded invariant checking of blackbox designs

被引：0

作者：

Herbstritt, Marc ^{[1
]}

Becker, Bernd ^{[1
]}

机构：

[1] Univ Freiburg, Inst Comp Sci, Hugstetter Str 55, D-79110 Freiburg, Germany

来源：

MTV 2005: SIXTH INTERNATIONAL WORKSHOP ON MICROPRESSOR TEST AND VERIFICATION: COMMON CHALLENGES AND SOLUTIONS, PROCEEDINGS | 2006年

关键词：

D O I：

暂无

中图分类号：

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

学科分类号：

0812 ;

摘要：

Design verification by property checking is a mandatory task during circuit design. In this context, Bounded Model Checking (BMC) has become popular for falsifying erroneous designs. Additionally, the analysis of partial designs, i.e., circuits that are not fully specified, has recently gained attraction. In this work we analyze how BMC can be applied to such partial designs. Our experiments show that even with the most simple modelling scheme, namely 01X-simulation, a relevant number of errors can be detected. Additionally, we propose a SAT-solver that directly can handle 01X-logic.

引用

页码：23 / +

页数：3

共 50 条

[41] SAT-based unbounded model checking of timed automata
Penczek, Wojciech
Szreter, Maciej
[J]. SEVENTH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2007, : 236 - 237
[42] Model checking with SAT-based characterization of ACTL formulas
Zhang, Wenhui
[J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2007, 4789 : 191 - 211
[43] Combining abstraction refinement and SAT-Based model checking
Amla, Nina
McMillan, Kenneth L.
[J]. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, 2007, 4424 : 405 - 419
[44] Efficient LTL compilation for SAT-based model checking
Armoni, R
Egorov, S
Fraer, R
Korchemny, D
Vardi, MY
[J]. ICCAD-2005: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, DIGEST OF TECHNICAL PAPERS, 2005, : 877 - 884
[45] Proving ∀μ-calculus properties with SAT-based model checking
Wang, BY
[J]. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 113 - 127
[46] Frontend model generation for SAT-based property checking
Wedler, M
Stoffel, D
Kunz, W
[J]. 2005 6TH INTERNATIONAL CONFERENCE ON ASIC PROCEEDINGS, BOOKS 1 AND 2, 2005, : 914 - 919
[47] Finding Attractors in Synchronous Multiple-Valued Networks Using SAT-based Bounded Model Checking
Dubrova, Elena
Liu, Ming
Teslenko, Maxim
[J]. JOURNAL OF MULTIPLE-VALUED LOGIC AND SOFT COMPUTING, 2012, 19 (1-3) : 109 - 131
[48] Finding Attractors in Synchronous Multiple-Valued Networks Using SAT-based Bounded Model Checking
Dubrova, Elena
Teslenko, Maxim
Ming, Liu
[J]. 40TH IEEE INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC ISMVL 2010, 2010, : 144 - 149
[49] Efficient SAT-based Circuit Initialization for Larger Designs
Sauer, Matthias
Reimer, Sven
Reddy, Sudhakar M.
Becker, Bernd
[J]. 2014 27TH INTERNATIONAL CONFERENCE ON VLSI DESIGN AND 2014 13TH INTERNATIONAL CONFERENCE ON EMBEDDED SYSTEMS (VLSID 2014), 2014, : 62 - 67
[50] Improved SAT based bounded model checking
Zhou, Conghua
Ding, Decheng
[J]. THEORY AND APPLICATIONS OF MODELS OF COMPUTATION, PROCEEDINGS, 2006, 3959 : 611 - 620

← 1 2 3 4 5 →