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.

翻译：几乎所有高效的硬件验证算法都是公式特定的，即考虑了当前公式的结构。因此，这些算法可被视为$\mathit{结构感知计算}$（SAC）。本文探讨了SAC与$\mathit{部分量词消解}$（PQE）之间的关系，后者是常规量词消解的推广。在PQE中，可以将公式的$\mathit{部分}$移出量词的辖域。插值可视为PQE的特例。本文的目标有二：首先，我们旨在说明基于PQE可以构建新的强大SAC方法。我们通过三个硬件验证问题（基于属性生成的测试、等价性验证和模型检验）阐释如何通过PQE实现SAC。其次，我们希望证明PQE求解本身亦可受益于SAC。为此，我们描述了一种基于SAC的新SAT过程，并利用它提出了一种结构感知的PQE算法。