Name
Abstract | ||
|---|---|---|
SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, there are applications, in particular in the area of partial design verification, where SAT formulas are not expressive enough and a description via Quantified Boolean Formulas (QBF) is much more adequate. In this paper we introduce incremental QBF solving and thereby make it usable as a core component of BMC. To do so, we realized an incremental version of the state-of-the-art QBF solver QuBE, allowing for the reuse of learnt information e.g. in the form of conflict clauses and solution cubes. As an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes) and thereby disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. In our experimental analysis, we compare different incremental approaches implemented in our BMC tool. BMC with incremental QBF turns out to be feasible for designs with more than 21,000 gates and 2,700 latches. Significant performance gains over non incremental QBF based BMC can be obtained on many benchmark circuits, in particular when using the so-called backward-incremental approach combined with incremental preprocessing. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1109/DATE.2012.6176547 | DATE |
Keywords | Field | DocType |
incremental fashion,incremental preprocessing,partial design,core component,sat formula,non incremental qbf,incremental qbf,indispensable core component,different incremental approach,bmc tool,incremental version,experimental analysis,sequential analysis,system on a chip,stability,power optimization,encoding,logic gate,power analysis,boolean functions,logic gates,observability,benchmark testing,formal verification,data preprocessing | Boolean function,System on a chip,Model checking,Computer science,Data pre-processing,Theoretical computer science,Solver,Benchmark (computing),Realizability,Formal verification | Conference |
ISSN | Citations | PageRank |
1530-1591 | 6 | 0.45 |
References | Authors | |
14 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paolo Marin | 1 | 67 | 6.83 |
| Christian Miller | 2 | 36 | 4.39 |
| Matthew Lewis | 3 | 107 | 6.37 |
| Bernd Becker | 4 | 855 | 73.74 |