This Article 
 Bibliographic References 
 Add to: 
Automated Verification of Behavioral Equivalence for Microprocessors
January 1994 (vol. 43 no. 1)
pp. 115-117

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.

[1] J.R. Burch et al., "Sequential Circuit Verification Using Symbolic Model Checking,"Proc. 27th Design Automation Conf., IEEE CS Press, 1990, pp. 46-51.
[2] F. Corella, "Automated verification of behavioral equivalence for microprocessors," RC 17751, IBM Res. Rep., revised Jan. 1993.
[3] F. Corella, "Case study in automated verification of behavioral equivalence: The Tamarack-3 microprocessor," RC 17922, IBM Res. Rep., Apr. 1992.
[4] F. Corella, "Correctness of a hardware verification procedure," RC 18358, IBM Res Rep., Sept. 1992.
[5] F. Corella, "Automated high-level verification against clocked algorithmic specifications," inProc. of Conf on Hardware Description Languages, 1993, pp. 135-142.
[6] O. Coudert and J. C. Madre, "A unified framework for the formal verification of sequential circuits," inProc. Int. Conf. Computer-Aided Design, 1990.
[7] W. A. Hunt, "FM8501: A verified microprocessor," Ph.D. dissertation, Univ. of Texas, Austin, 1985.
[8] J. J. Joyce, "Multi-level verification of microprocessor-based systems," Tech. Rep. 195., Univ. Cambridge, Computer Lab., Ph.D. dissertation, May 1990.
[9] K. J. Supowit and S. J. Friedman, "A new method for verifying sequential circuits," inProc. 23rd Design Automation Conf., 1986, pp. 200-205.
[10] H. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. Sangiovanni-Vincentelli, "Implicit state enumeration of finite state machines using BDD's," inProc. IEEE Int. Conf. Comput.-Aided Design, Nov. 1990, pp. 130-133.
[11] F. Van Aelten, J. Allen, and S. Devadas, "Verification of relations between synchronous machines," inProc. Int. Conf. Computer-Aided Design, pp. 380-383.

Index Terms:
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," IEEE Transactions on Computers, vol. 43, no. 1, pp. 115-117, Jan. 1994, doi:10.1109/12.250616
Usage of this product signifies your acceptance of the Terms of Use.