A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor
One obstacle to mathematical verification of industrial hard- ware designs is that the commercial hardware description languages in which they are usually encoded are too complicated and poorly spec- ified to be readily susceptible to formal analysis. As an alternative to these commercial languages, AMD1 has developed an RTL language for microprocessor designs that is simple enough to admit a clear semantic definition, providing a basis for formal verification. We describe a me- chanical proof system for designs represented in this language, consisting of a translator to the ACL2 logical programming language and a method- ology for verifiying properties of the resulting programs using the ACL2 prover. As an illustration, we present a proof of IEEE compliance of the floating-point adder of the AMD Athlon processor.
KeywordsClose Path Left Shift Sequential Assignment Combinational Circuit Simple Pipeline
Unable to display preview. Download preview PDF.
- 1.Institute of Electrical and Electronic Engineers, “IEEE Standard for Binary Floating Point Arithmetic”, Std. 754-1985, New York, NY, 1985.Google Scholar
- 2.Intel Corporation, Pentium Family User’s Manual, Volume 3: Architecture and Programming Manual, 1994.Google Scholar
- 3.Kaufmann, M., Manolios, P., and Moore, J, Computer-Aided Reasoning: an Approach, Kluwer Academic Press, 2000.Google Scholar
- 4.Moore, J, Lynch, T., and Kaufmann, M., “A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating Point Division Algorithm”, IEEE Transactions on Computers, 47:9, September, 1998.Google Scholar
- 5.Oberman, S., Hesham, A., and Flynn, M., “The SNAP Project: Design of Floating Point Arithmetic Units”, Computer Systems Lab., Stanford U., 1996.Google Scholar
- 7.Russinoff, D., “A Mechanically Checked Proof of IEEE Compliance of the AMD-K7 Floating Point Multiplication, Division, and Square Root Algorithms”. See http://www.onr.com/user/russ/david/k7-div-sqrt.html.
- 8.Russinoff, D. and Flatau, A., “RTL Verification: A Floating-Point Multiplier”, in Kaufmann, M., Manolios, P., and Moore, J, eds., Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Press, 2000. See http://www.onr.com/user/russ/david/acl2.html.
- 9.Russinoff, D., “An ACL2 Library of Floating-Point Arithmetic”, 1999. See http://www.cs.utexas.edu/users/moore/publications/others/fp-README.html.