论文标题
一组完整的属性
Generation Of A Complete Set Of Properties
论文作者
论文摘要
正式验证的问题之一是，由于规格不完整，它在功能上没有完成。符合不完整规范的实施可能仍然有很多错误。在测试中，通过用$ \ mathit {结构} $替换功能完整性来解决此问题。后者是通过生成一组测试来探测每一个设计实现的方法来实现的。我们表明可以在形式验证中使用类似的方法。这里的想法是生成手头实现的属性，该属性不暗示规范。找到这样的属性意味着规范尚未完成。如果这是$ \ mathit {不需要的} $属性，则实现是错误的。否则，需要添加新的规范属性。与设计的不同部分相关的实现属性的生成，然后添加新规范属性会产生$ \ mathit {structurolly} $ - $ \ MATHIT {完整\：Specification} $。实现属性由$ \ mathit {partial \：量词\：消除} $构建，这是一种仅从量化器范围中取出的一部分公式的技术。实现属性是通过将部分量化器消除应用于定义实施“真实表”的公式来生成的。我们展示了我们的方法如何在组合和顺序电路的规范上起作用。
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.
