Structure-Aware Computing, Partial Quantifier Elimination And SAT
For hardware verification practitioners, this work proposes a new paradigm (SAC via PQE) that could accelerate semantic reasoning, but the results are conceptual without concrete performance numbers.
The paper introduces structure-aware computing (SAC), which exploits formula structure to obtain semantic results faster, and shows that partial quantifier elimination (PQE) enables SAC for verification problems like property generation, equivalence checking, and model checking. It also demonstrates that SAT-based techniques can improve structure-aware PQE solving.
Typically, a practical algorithm of hardware verification obtains a semantic result by being applied to a particular formula $F$. That is, although this algorithm uses the specifics of $F$ (sometimes inadvertently), its result holds for all formulas logically equivalent to $F$. We refer to computations that get a semantic result by intentionally exploiting the specifics of $F$ as structure-aware computing (SAC). Arguably, using SAC allows one to get a semantic result faster. We show that partial quantifier elimination (PQE), a generalization of quantifier elimination, can be used for SAC. The objective of this paper is twofold. First, we explain how SAC is performed by PQE by the example of three verification problems (property generation, equivalence checking and model checking). Second, we argue that PQE solving itself can benefit from SAC. We use SAT solving to introduce a technique that can be also applied in structure-aware PQE solving.