论文标题
关于用不完整规范验证设计
On Verifying Designs With Incomplete Specification
论文作者
论文摘要
规范的不完整$ \ mathit {spec} $造成了两个问题。首先，$ \ mathit {spec} $的实现$ \ mathit {stranp} $可能有一些$ \ mathit {不需要的} $ properties $ \ mathit {spec} $不禁止。其次，$ \ mathit {strans} $可能会破坏不在$ \ mathit {spec} $中的$ \ mathit {所需} $属性。无论哪种情况，$ \ mathit {spec} $都无法公开$ \ mathit {inpper} $的错误。在较早的论文中，我们通过一种称为部分量化器消除（PQE）的技术解决了上述第一个问题。与完整的量化宽松相比，在PQE中，一个仅一小部分公式从量词范围中取出。我们使用pqe生成$ \ mathit {strank} $的属性，即，$ \ mathit {一致} $带有$ \ mathit {strans {strans} $。产生不需要的属性意味着$ \ athit {strans} $是错误的。在本文中，我们通过使用PQE生成错误属性（即$ \ Mathit {Inconcessent} $与$ \ Mathit {impl} $的属性，我们解决了上述第二个问题。这样的属性旨在模仿$ \ mathit {spec} $的丢失属性，这些属性不受$ \ mathit {stramp} $（如果有）不满足。通过修改描述$ \ mathit {strans} $的“真实表”的一块量化公式并将这一部分删除的量化范围来生成错误的属性。通过修改该公式的不同部分，可以生成一组“结构完整”的假属性。通过生成测试检测$ \ Mathit {Impl} $的假属性，一个人会产生高质量的测试集。我们将我们的方法应用于组合和顺序电路的验证。
Incompleteness of a specification $\mathit{Spec}$ creates two problems. First, an implementation $\mathit{Impl}$ of $\mathit{Spec}$ may have some $\mathit{unwanted}$ properties that $\mathit{Spec}$ does not forbid. Second, $\mathit{Impl}$ may break some $\mathit{desired}$ properties that are not in $\mathit{Spec}$. In either case, $\mathit{Spec}$ fails to expose bugs of $\mathit{Impl}$. In an earlier paper, we addressed the first problem above by a technique called Partial Quantifier Elimination (PQE). In contrast to complete QE, in PQE, one takes out of the scope of quantifiers only a small piece of the formula. We used PQE to generate properties of $\mathit{Impl}$ i.e. those $\mathit{consistent}$ with $\mathit{Impl}$. Generation of an unwanted property means that $\mathit{Impl}$ is buggy. In this paper, we address the second problem above by using PQE to generate false properties i.e those that are $\mathit{inconsistent}$ with $\mathit{Impl}$. Such properties are meant to imitate the missing properties of $\mathit{Spec}$ that are not satisfied by $\mathit{Impl}$ (if any). A false property is generated by modifying a piece of a quantified formula describing 'the truth table' of $\mathit{Impl}$ and taking this piece out of the scope of quantifiers. By modifying different pieces of this formula one can generate a "structurally complete" set of false properties. By generating tests detecting false properties of $\mathit{Impl}$ one produces a high quality test set. We apply our approach to verification of combinational and sequential circuits.
