This work presents a novel approach for evaluatingthe quality of the model checkingpro cess. Given a model of a design (or
implementation) and a temporal logic formula that describes a specification, model checkingde termines whether the model satisfies
the specification. Assume that all specification formulas were successfully checked for the implementation. Are we sure that
the implementation is correct? If the specification is incomplete, we may fail to find an error in the implementation. On
the other hand, if the specification is complete, then the model checkingpro cess can be stopped without adding more specification
formulas. Thus, knowingwh ether the specification is complete may both avoid missed implementation errors and save precious
verification time.
The completeness of a specification with respect to a given implementation is determined as follows. The specification formula
is first transformed into a tableau. The simulation preorder is then used to compare the implementation model and the tableau
model. We suggest four comparison criteria, each revealinga certain dissimilarity between the implementation and the specification.
If all comparison criteria are empty, we conclude that the tableau is bisimilar to the implementation model and that the specification
fully describes the implementation. We also conclude that there are no redundant states in the implementation. The method
is exemplified on a small hardware example. We implemented our method symbolically as an extension to SMV. The implementation
involves efficient OBDD manipulations that reduce the number of OBDD variables from 4n to 2n.
Acknowledgment We thank Ilan Beer for suggesting to look into the problem of coverage in model checking.The first author thanks Galileo Technology
for the opportunity to work on the subject.