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, which are based on Goldschmidt's Algorithm, 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 considerable more abstract. Therefore, we begin by developing a theory of bit vectors and their role in floating-point representations and rounding, extending our previous work in conection with the K5 FPU. We then present the hardware model and a rigorous and detailed 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.
Full paper: ps, pdf (appeared in the LMS Journal of Computation and Mathematics 1: 148-200, December, 1998.)