Bounded Model Checking (BMC) is a major verification method for finding errors in sequential circuits. BMC accomplishes this by iteratively unfolding a circuit k times, adding the negated property, and finally converting the BMC instance into a sequence of satisfiability (SAT) problems. When considering incomplete designs (i.e. those containing so-called blackboxes), we rather need the logic of Quantified Boolean Formulas (QBF) to obtain a more precise modeling of the unknown behavior of the blackbox. Here, we answer the question of unrealizability of a property, where finding a path of length k proves that the property is violated regardless of the implementation of the blackbox. To boost this task, solving blackbox BMC problems incrementally has been shown to be feasible [3], although the restrictions required in the preprocessing phase reduce its effectiveness. In this paper we enhance the verification procedure when using an off-the-shelf QBF solver, through a stronger preprocessing of the QBF formulas applied in an incremental fashion. © 2012 Springer-Verlag.
CITATION STYLE
Marin, P., Miller, C., & Becker, B. (2012). Incremental QBF preprocessing for partial design verification (Poster presentation). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7317 LNCS, pp. 473–474). https://doi.org/10.1007/978-3-642-31612-8_41
Mendeley helps you to discover research relevant for your work.