Virtually all efficient algorithms of hardware verification are somewhat formula-specific i.e, try to take into account the structure of the formula at hand. So, those algorithms can be viewed as $\mathit{structure}$-$\mathit{aware}$ $\mathit{computing}$ (SAC). We relate SAC and $\mathit{partial}$ $\mathit{quantifier}$ $\mathit{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) and SAT to explain how SAC is performed by PQE. Second, we want to demonstrate that PQE solving $\mathit{itself}$ can benefit from SAC. To this end, we describe a technique meant for building structure-aware SAT solvers that paves the way to structure-aware PQE solving.

翻译：几乎所有高效的硬件验证算法都在某种程度上是针对特定公式的，即试图考虑当前公式的结构。因此，这些算法可视为$\mathit{结构感知计算}$（SAC）。本文探讨SAC与$\mathit{部分量词消解}$（PQE）之间的关联，后者是常规量词消解的推广形式。在PQE中，可将公式的$\mathit{部分}$内容移出量词作用域，而插值可视为PQE的特例。本文目标有二：其一，论证如何通过PQE形式化表述新型高效的SAC方法。我们通过三个硬件验证问题（基于属性生成的测试、等价性验证与模型检测）及SAT问题，阐释PQE如何实现SAC；其二，证明PQE求解$\mathit{本身}$可受益于SAC。为此，我们描述了一种构建结构感知SAT求解器的技术，为发展结构感知PQE求解器奠定基础。