By structure-aware computing (SAC) we mean computing that is formula-specific i.e., takes into account the structure of the formula at hand. Virtually all efficient algorithms of hardware verification employ some form of SAC. We relate SAC to $\mathit{partial}$ $\mathit{quantifier}$ $\mathit{elimination}$ (PQE). The latter is a generalization of regular quantifier elimination where one can take a $\mathit{part}$ of the formula out of the scope of quantifiers. The objective of this paper is to emphasize the significance of studying PQE for enhancing the $\mathit{existing}$ methods of SAC and creating $\mathit{new}$ ones. First, we show that interpolation (that can be viewed as an instance of SAC) is a special case of PQE. Then we describe application of SAC by PQE to three different problems of hardware verification: property generation, equivalence checking and model checking. Besides, we discuss using SAC by PQE for SAT solving.

翻译：结构感知计算（SAC）是指针对特定公式的计算，即考虑当前公式的结构。几乎所有高效的硬件验证算法都采用了某种形式的SAC。我们将SAC与部分量词消解（PQE）联系起来。后者是常规量词消解的推广，允许将公式的一部分移出量词的作用域。本文的目标在于强调研究PQE对于增强现有SAC方法及创建新方法的重要意义。首先，我们证明插值（可视为SAC的一个实例）是PQE的特例。随后，我们描述了通过PQE实现SAC在硬件验证三个不同问题中的应用：属性生成、等价性检验与模型检验。此外，我们还探讨了通过PQE实现SAC在SAT求解中的应用。