Abstract
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.
AMD, the AMD logo and combinations thereof, AMD-K5, and AMD Athlon are trademarks of Advanced Micro Devices, Inc.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Institute of Electrical and Electronic Engineers, “IEEE Standard for Binary Floating Point Arithmetic”, Std. 754-1985, New York, NY, 1985.
Intel Corporation, Pentium Family User’s Manual, Volume 3: Architecture and Programming Manual, 1994.
Kaufmann, M., Manolios, P., and Moore, J, Computer-Aided Reasoning: an Approach, Kluwer Academic Press, 2000.
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.
Oberman, S., Hesham, A., and Flynn, M., “The SNAP Project: Design of Floating Point Arithmetic Units”, Computer Systems Lab., Stanford U., 1996.
Russinoff, D., “A Mechanically Checked Proof of IEEE Compliance of the AMD-K5 Floating Point Square Root Microcode”, Formal Methods in System Design 14 (1):75–125, January 1999. See http://www.onr.com/user/russ/david/fsqrt.html.
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.
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.
Russinoff, D., “An ACL2 Library of Floating-Point Arithmetic”, 1999. See http://www.cs.utexas.edu/users/moore/publications/others/fp-README.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Russinoff, D.M. (2000). A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor. In: Hunt, W.A., Johnson, S.D. (eds) Formal Methods in Computer-Aided Design. FMCAD 2000. Lecture Notes in Computer Science, vol 1954. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40922-X_3
Download citation
DOI: https://doi.org/10.1007/3-540-40922-X_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41219-9
Online ISBN: 978-3-540-40922-9
eBook Packages: Springer Book Archive