A Case Study in Formal Verification of Register-Transfer Logic with ACL2: The Floating Point Adder of the AMD Athlon TM Processor

  • David M. Russinoff
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)


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.


Close Path Left Shift Sequential Assignment Combinational Circuit Simple Pipeline 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Institute of Electrical and Electronic Engineers, “IEEE Standard for Binary Floating Point Arithmetic”, Std. 754-1985, New York, NY, 1985.Google Scholar
  2. 2.
    Intel Corporation, Pentium Family User’s Manual, Volume 3: Architecture and Programming Manual, 1994.Google Scholar
  3. 3.
    Kaufmann, M., Manolios, P., and Moore, J, Computer-Aided Reasoning: an Approach, Kluwer Academic Press, 2000.Google Scholar
  4. 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. 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
  6. 6.
    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 Scholar
  7. 7.
    Russinoff, D., “A Mechanically Checked Proof of IEEE Compliance of the AMD-K7 Floating Point Multiplication, Division, and Square Root Algorithms”. See
  8. 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
  9. 9.
    Russinoff, D., “An ACL2 Library of Floating-Point Arithmetic”, 1999. See

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • David M. Russinoff
    • 1
  1. 1.Advanced Micro Devices, Inc.Austin

Personalised recommendations