A Simple Theorem Prover Based on symbolic Trajectory Evaluation and OBDDs

Formal hardware verification based on symbolic trajectory evaluation shows considerable promise in verifying medium to large scale VLSI designs with a high degree of automation. However, in order to verify today's designs, a method for composing partial verification results is needed. One way of accomplishing this is to use a general purpose theorem prover to combine the verification results obtained by other tools. However, a special purpose theorem prover is more attractive since it can more easily exploit symbolic trajectory evaluation (and may be easier to use). Consequently we explore the possibility of developing a much simpler, but more tailor made, theorem prover designed specifically for combining verification results based on trajectory evaluation. In the paper we discuss the underlying inference rules of the prover as well as more practical issues regarding the user interface. We finally conclude with a couple of examples in which we are able to verify designs that could not have been verified directly. In particular, the complete verification of a 64 bit multiplier takes approximately 15 minutes on a Sparc 10 machine.