This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verifying the FM9801 Microarchitecture
May/June 1999 (vol. 19 no. 3)
pp. 47-55
Designers use formal logic and a theorem prover to verify that a complex microarchitecture always implements its instruction set correctly. Hardware verification accounts for a considerable portion of the costs in the microprocessor design process. Traditionally, designers have verified microprocessor designs using simulation techniques that help find most design faults. However, simulation never guarantees the correct operation of the final product. Some design faults are very difficult to detect by simulation; they may slip through the verification process into manufactured chips, raising costs. We believe that verification costs can be reduced by the judicious application of formal methods, which should lower the overall costs of design.

1. M. Kaufmann and J.S. Moore, "ACL2: An Industrial Strength Version of Nqthm," Proc. 11th Ann. Conf. Computer Assurance, COMPASS-96, IEEE Computer Soc. Press, Los Alamitos, Calif., June 1996, pp. 23-34.
2. B.C. Brock and W.A. Hunt, Jr., "The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor," Formal Methods in System Design, Kluwer Academic Publishers, Dordrecht, Netherlands, Vol. 11, Issue 1, July, 1997, pp. 71-104.
3. M.K. Srivas and S.P. Miller, Formal Verification of an Avionics Microprocessor, Tech. Report CSL-95-04, SRI Int'l Computer Sci. Laboratory, Menlo Park, Calif., June 1995.
4. B. Brock, M. Kaufmann, and J S. Moore, "ACL2 Theorems about Commercial Microprocessors," Formal Methods in Computer-Aided Design (FMCAD '96), M. Srivas and A. Camilleri, eds. , pp. 275-293. Springer-Verlag, Nov. 1996.
5. K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
6. Formal Semantics for VHDL, C.D. Koos and P.T. Breuer, eds., Kluwer, 1995.
7. M.J.C. Gordon, "The Semantic Challenge of Verilog HDL," Proc. 10th Ann. IEEE Symp. Logic in Computer Sci., (LICS'95), IEEE CS Press, pp. 136-145.
8. B.C. Brock, W.A. Hunt, Jr., and M. Kaufmann, The FM9001 Microprocessor Proof, Tech. Report 86, Computational Logic, Inc., Austin, Tex., Dec. 1994, http://www.cli.com/reports/files86.ps.
9. J.R. Burch and D.L. Dill, "Automatic Verification of Pipelined Microprocessor Control," Proc. Computer-Aided Verification (CAV 94), Springer-Verlag, 1994, pp. 68-80.
10. J.R. Burch, "Techniques for Verifying Superscalar Microprocessors," Proc. 33rd Design Automation Conf. (DAC 96), ACM Press, 1996, pp. 552-557.
11. J. Sawada and W.A. HuntJr., "Processor Verification with Precise Exceptions and Speculative Execution," Proc. Computer-Aided Verification (CAV 98), Springer-Verlag, 1998, pp. 135-146.
12. L.-N. Lee, A.R. Hammons, F.-W. Sun, and M. Eroz, “Application and Standardization of Turbo Codes in Third Generation High-Speed Wireless Data Services,” IEEE Trans. Vehicular Technology, vol. 49, no. 6, pp. 2198-2207, Nov. 2000.
13. J. Sawada and W. Hunt, Jr., "Trace Table Based Approach for Pipelined Microprocessor Verification," Proc. Computer-Aided Verification, CAV '97, Lecture Notes in Computer Science 1254, Springer Verlag, 1997, pp. 364-375.
14. K.L. McMillan, "Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking," Proc. Workshop on Formal Techniques for Hardware and Hardware-Like Systems,Marstrand, Sweden; published by Dept. of Computer Science, Chalmers Univ. of Tech nology, June 1998.

Citation:
Warren A. Hunt, Jr., Jun Sawada, "Verifying the FM9801 Microarchitecture," IEEE Micro, vol. 19, no. 3, pp. 47-55, May-June 1999, doi:10.1109/40.768503
Usage of this product signifies your acceptance of the Terms of Use.