Structure-Aware Computing, Partial Quantifier Elimination And SAT

Virtually all efficient algorithms of hardware verification are formula-specific i.e., take into account the structure of the formula at hand. So, those algorithms can be viewed as $\mathit{structure}$-$\mathit{aware\;computing}$ (SAC). We relate SAC and $\mathit{partial\;quantifier\;elimination}$ (PQE), a generalization of regular quantifier elimination. In PQE, one can take a $\mathit{part}$ of the formula out of the scope of quantifiers. Interpolation can be viewed as a special case of PQE. The objective of this paper is twofold. First, we want to show that new powerful methods of SAC can be formulated in terms of PQE. We use three hardware verification problems (testing by property generation, equivalence checking and model checking) to explain how SAC is performed by PQE. Second, we want to demonstrate that PQE solving itself can benefit from SAC. To this end, we describe a new SAT procedure based on SAC and then use it to introduce a structure-aware PQE algorithm.