We study partial quantifier elimination (PQE) for propositional CNF formulas with existential quantifiers. PQE is a generalization of quantifier elimination where one can limit the set of clauses taken out of the scope of quantifiers to a small subset of clauses. The appeal of PQE is that many verification problems (e.g. equivalence checking and model checking) can be solved in terms of PQE and the latter can be dramatically simpler than full quantifier elimination. We show that PQE can be used for property generation that can be viewed as a generalization of testing. The objective here is to produce an $\mathit{unwanted}$ property of a design implementation thus exposing a bug. We introduce two PQE solvers called $\mathit{EG}$-$\mathit{PQE}$ and $\mathit{EG}$-$\mathit{PQE}^+$. $\mathit{EG}$-$\mathit{PQE}$ is a very simple SAT-based algorithm. $\mathit{EG}$-$\mathit{PQE}^+$ is more sophisticated and robust than $\mathit{EG}$-$\mathit{PQE}$. We use these PQE solvers to find an unwanted property (namely, an unwanted invariant) of a buggy FIFO buffer. We also apply them to invariant generation for sequential circuits from a HWMCC benchmark set. Finally, we use these solvers to generate properties of a combinational circuit that mimic symbolic simulation.

翻译：我们研究命题CNF公式中带存在量词的部分量词消去（PQE）。PQE是量词消去的一种泛化形式，允许将需要从量词作用域中移除的子句集限制为少量子集。PQE的吸引力在于，许多验证问题（例如等价性检查和模型检验）可通过PQE求解，且后者比完全量词消去简单得多。我们证明PQE可用于性质生成，这可以视为测试的泛化形式。其目标是生成设计实现的不期望性质，从而暴露缺陷。我们介绍两种PQE求解器：$\mathit{EG}$-$\mathit{PQE}$和$\mathit{EG}$-$\mathit{PQE}^+$。$\mathit{EG}$-$\mathit{PQE}$是一种极简的基于SAT的算法，$\mathit{EG}$-$\mathit{PQE}^+$比$\mathit{EG}$-$\mathit{PQE}$更复杂且鲁棒性更强。我们利用这些PQE求解器寻找带缺陷FIFO缓冲器的不期望性质（即不期望不变式），并将其应用于HWMCC基准测试集序列电路的不变式生成。最后，我们使用这些求解器生成组合电路的属性，以模拟符号仿真。