AUTOMATED VERIFICATION OF BEHAVIORAL EQUIVALENCE FOR MICROPROCESSORS

We present a new method for verifying in a fully automated way that two synchronous sequential circuits have the same input/output behavior. The method applies to designs in which a distinction between data path and control can be made, and in particular to microprocessors. The verification is carried out at the register-transfer level. In contrast with previous methods, our procedure is not limited by the total number of latches in the circuit: it runs in time independent of the width of the data path. A price has to be paid for this: the procedure does not always terminate, and may produce false negatives. We argue, however, that these problems should not come up when verifying general purpose microprocessors. We have implemented the procedure in Prolog on an IBM RS/6000 workstation, and have tried it on the Tamarack-3 microprocessor previously verified by Joyce with the interactive theorem prover HOL at the University of Cambridge. We have verified the equivalence of several alternative implementations to the original one in times ranging from 11 to 26 s, and we have detected the errors in several incorrect implementations, in times ranging from 1 to 26 s.