On Verifying Designs With Incomplete Specification

Abstract

Incompleteness of a specification $Spec$ creates two problems. First, an implementation $Impl$ of $Spec$ may have some $unwanted$ properties that $Spec$ does not forbid. Second, $Impl$ may break some $desired$ properties that are not in $Spec$. In either case, $Spec$ fails to expose bugs of $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 $Impl$ i.e. those $consistent$ with $Impl$. Generation of an unwanted property means that $Impl$ is buggy. In this paper, we address the second problem above by using PQE to generate false properties i.e those that are $inconsistent$ with $Impl$. Such properties are meant to imitate the missing properties of $Spec$ that are not satisfied by $Impl$ (if any). A false property is generated by modifying a piece of a quantified formula describing 'the truth table' of $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 $Impl$ one produces a high quality test set. We apply our approach to verification of combinational and sequential circuits.

arXiv admin note: text overlap with arXiv:2004.05853