loading...
On SAT-based Bounded Invariant Checking of Blackbox Designs
Austin, Texas November 03-November 05
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MTV.2005.16Sixth International Workshop on Micro ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Marc Herbstritt, Albert-Ludwigs-University, Germany
Bernd Becker, Albert-Ludwigs-University, Germany
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 01Xsimulation, a relevant number of errors can be detected. Additionally, we propose a SAT-solver that directly can handle 01X-logic.
Citation:
Marc Herbstritt, Bernd Becker, "On SAT-based Bounded Invariant Checking of Blackbox Designs," mtv, pp.23-28, Sixth International Workshop on Microprocessor Test and Verification (MTV'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.