Hostname: page-component-669899f699-cf6xr Total loading time: 0 Render date: 2025-04-26T00:19:50.273Z Has data issue: false hasContentIssue false
  • English
  • Français

A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor

Published online by Cambridge University Press:  01 February 2010

David M. Russinoff
David M. Russinoff
Affiliation:
Advanced Micro Devices, Inc., 5900 E. Ben White Blvd, MS 625, Austin, TX 78741, U.S.A., [email protected]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We describe a mechanically verified proof of correctness of the floating point multiplication, division, and square root instructions of the AMD-K7 microprocessor. The instructions are implemented in hardware and represented here by register-transfer level specifications, the primitives of which are logical operations on bit vectors. On the other hand, the statements of correctness, derived from IEEE Standard 754, are arithmetic in nature and considerably more abstract. Therefore, we begin by developing a theory of bit vectors and their role in floating point representations and rounding. We then present the hardware model and a rigorous proof of its correctness. All of our definitions, lemmas and theorems have been formally encoded in the ACL2 logic, and every step in the proof has been mechanically checked with the ACL2 prover.

Type
Research Article
Information
LMS Journal of Computation and Mathematics , Volume 1 , 1998 , pp. 148 - 200
Copyright
Copyright © London Mathematical Society 1998

References

1. Anderson, S.F., Earle, J.G., Goldschmidt, R.E. and Powers, D.M., ‘The IBM System/360 Model 91 Floating Point Execution Unit’, IBM Journal of Research and Development, 11 (January 1967) 34–53.Google Scholar
2. Boyer, R.S. and Moore, J., A computational logic handbook(Academic Press, Boston, MA, 1988).Google Scholar
3. Bryant, R.E., ‘Verification of arithmetic functions with binary moment diagrams’, Technical Report CMU-CS-94-160, School of Computer Science, Carnegie-Mellon University, 1994.Google Scholar
4. Clarke, E.M. and Zhao, X., ‘Word level symbolic model checking: a new approach for verifying arithmetic circuits’, Technical Report CMU-CS-95-161, School of Computer Scence, Carnegie-Mellon University, 1995.Google Scholar
5. Institute of Electrical and Electronic Engineers, ‘IEEE Standard for Binary Floating Point Arithmetic’, Std. 754-1985, (IEEE, New York, NY, 1985).Google Scholar
6. 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 (September, 1998).Google Scholar
7. Oberman, S.F., ‘Division and square root for the AMD-K7 FPU’ (Advanced Micro Devices, Milpitas, CA, March 1997).Google Scholar
8. Russinoff, D.M., ‘A mechanically checked proof of IEEE compliance of the AMD-K5 floating point square root microcode’, Formal Methods in System Design, to appear. http://www.onr.com/user/russ/david/fsqrt.html.Google Scholar
9. Steele, G.L., Jr., Common Lisp The Language 2nd edition (Digital Press, Waltham MA, 1990).Google Scholar
Supplementary material: File

Russinoff Appendix

Appendix

Download Russinoff Appendix(File)
File 947.9 KB