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