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.

翻译：通常，硬件验证的实用算法通过应用于特定公式$F$来获得语义结果。也就是说，尽管该算法利用了$F$的特性（有时是无意的），但其结果对逻辑等价于$F$的所有公式均成立。我们将通过刻意利用$F$的特性来获取语义结果的计算称为结构感知计算（SAC）。可以说，使用SAC能更快地获取语义结果。本文证明，作为量词消去推广形式的部分量词消去（PQE）可用于实现SAC。本文目标有二：第一，通过三个验证问题（属性生成、等价性检验与模型检验）的实例，阐释PQE如何执行SAC；第二，论证PQE求解本身也能从SAC中获益。我们以SAT求解为工具，提出一种可应用于结构感知PQE求解的技术。