Proving QBF-hardness in Bounded Model Checking for Incomplete Designs

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.