Generation Of A Complete Set Of Properties

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.