Generation Of A Complete Set Of Properties
share
One of the problems of formal verification is that it is not functionally complete. The fact that a set of properties of a specification holds for a design implementation, in general, does not mean that this implementation is bug-free. In testing, this issue is addressed by replacing functional completeness with 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 specification properties. Finding such a property means that the specification is not complete. If this is an unwanted property, then 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 structurally-complete specification. Implementation properties are built by 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.
READ FULL TEXT