生成一组完整的属性

摘要：

形式化验证存在的问题之一是由于规格说明的不完备性而导致功能上不完备。一个满足不完整规范的实现可能仍然有很多bug。在测试中，通过将功能完整性替换为$\mathit{structural}$来解决此问题。后者是通过生成一组测试来探测设计实现的每一部分来实现的。我们表明，类似的方法可以用于形式化验证。这里的想法是生成一个在规范中没有暗示的实现的属性。找到这样的属性意味着规范是不完整的。如果这是一个$\mathit{unwanted}$属性，则该实现存在错误。否则，需要添加新的规范属性。生成与设计的不同部分相关的实现属性，然后添加新的规范属性，生成$\mathit{structurally}$ - $\mathit{complete\:specification}$。实现属性是由$\mathit{partial\: quantifier\:elimination}$构建的，这是一种仅将公式的一部分从限定符的范围中取出的技术。通过将部分量词消去应用于定义实现的“真值表“的公式来生成实现属性。我们展示了我们的方法是如何工作的组合和时序电路的规格。

英文摘要：

One of the problems of formal verification is that it is not functionally complete due the incompleteness of specifications. An implementation meeting an incomplete specification may still have a lot of bugs. In testing, this issue is addressed by replacing functional completeness with $\mathit{structural}$ one. The latter is achieved by generating a set of tests probing every piece of a design implementation. We show that a similar approach can be used in formal verification. The idea here is to generate a property of the implementation at hand that is not implied by the specification. Finding such a property means that the specification is not complete. If this is an $\mathit{unwanted}$ property, the implementation is buggy. Otherwise, a new specification property needs to be added. Generation of implementation properties related to different parts of the design followed by adding new specification properties produces a $\mathit{structurally}$-$\mathit{complete\:specification}$. Implementation properties are built by $\mathit{partial\: quantifier\:elimination}$, a technique where only a part of the formula is taken out of the scope of quantifiers. An implementation property is generated by applying partial quantifier elimination to a formula defining the "truth table" of the implementation. We show how our approach works on specifications of combinational and sequential circuits.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。