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

共 12 条

[1] ABRAMOVICI M, 1990, DIGIAL SYSTEMS TESTI
[2] BIERE A, 1999, DES AUT C
[3] BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819
[4] SYMBOLIC MODEL CHECKING FOR SEQUENTIAL-CIRCUIT VERIFICATION
BURCH, JR
CLARKE, EM
LONG, DE
MCMILLAN, KL
DILL, DL
[J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 1994, 13 (04) : 401 - 424
[5] Clarke EM, 1999, MODEL CHECKING, P1
[6] Clarke Teresa E., 2001, Current Topics in Medicinal Chemistry, V1, P7, DOI 10.2174/1568026013395623
[7] JAIN A, 2000, VLSI TEST S, P263
[8] KUEHLMANN A, 2002, IEEE T CAD
[9] MOSKEWICZ MW, 2001, DES AUT C
[10] Nopper T, 2004, LECT NOTES COMPUT SC, V3312, P290

← 1 2 →