  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.
