Issue No. 01 - January (1994 vol. 43)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.250616
<p>Presents 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 that is 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 J.J. Joyce (1990) 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.</p>
microprocessor chips; logic testing; sequential circuits; flip-flops; abstract data types; artificial intelligence; circuit CAD; finite state machines; formal verification; IBM computers; logic programming; automated hardware verification; behavioral equivalence; interactive theorem prover; synchronous sequential circuits; input/output behavior; data path; data control; register-transfer level; latches; nonterminating procedures; false negatives; Prolog; IBM RS/6000 workstation; Tamarack-3 microprocessor; general purpose microprocessor design; HOL; logic programming; incorrect implementations; abstract data types; artificial intelligence; computer-aided design; finite state machines; 1 to 26 s.
F. Corella, "Automated Verification of Behavioral Equivalence for Microprocessors," in IEEE Transactions on Computers, vol. 43, no. , pp. 115-117, 1994.