Paper Info
Title
Proving QBF-hardness in Bounded Model Checking for Incomplete Designs
Abstract
Bounded Model Checking (BMC) is a major verification technique for finding errors in sequential circuits by unfolding the design iteratively and converting the BMC instances into Boolean satisfiability (SAT) formulas. Here, we consider incomplete designs (i.e. those containing so-called black boxes) where the verification task is to prove unrealizability of a property. A property is called unrealizable by an incomplete design, if there is an error which can not be compensated by any implementation of the black boxes. While 01X-modeling of the unknown behavior of the black boxes yields easy-to-solve SAT problems, the logic of quantified Boolean formulas (QBF) is needed for 01X-hard problems to obtain a more precise modeling. However, QBF-modeling does not guarantee success in proving unrealizability. To this purpose, we introduce the concept of QBF-hardness in this paper, a classification of problems for which the QBF-based modeling does not provide a result. Furthermore, we present an iterative method to prove the QBF-hardness. We provide a first practical example (a parameterized incomplete arbiter bus system) to demonstrate the concept.
Year
DOI
Venue
2013
10.1109/MTV.2013.11
Microprocessor Test and Verification
Keywords
Field
DocType
Boolean functions,iterative methods,logic design,sequential circuits,01X-modeling,Boolean satisfiability formulas,black boxes,bounded model checking,iterative method,quantified Boolean formulas,sequential circuits,QBF-hardness,black box,bounded model checking,incomplete design
Black box (phreaking),Arbiter,Parameterized complexity,Model checking,Computer science,Iterative method,Boolean satisfiability problem,Algorithm,Theoretical computer science,Black box,Bounded function
Conference
ISSN
Citations 
PageRank 
1550-4093
4
0.40
References 
Authors
14
3
Name
Order
Citations
PageRank
Christian Miller1364.39
Christoph Scholl234632.07
Bernd Becker385573.74