We present a rigorous mathematical proof of the correctness of the FSQRT instruction of the AMD K5 microprocessor. The instruction is represented as a program in a formal language that was designed for this purpose, based on the K5 microcode and the architecture of its FPU. We prove a statement of its correctness that corresponds directly with the IEEE standard. We also derive an equivalent formulation, expressed in terms of rational arithmetic, which has been encoded as a formula in the ACL2 logic and mechanically verified with the ACL2 prover. Finally, we describe a microcode modification that was implemented as a result of this analysis in order to ensure the correctness of the instruction.
Full paper: ps, pdf
(appeared in Formal Methods in System Design, 14:1, January 1999)
Slides
Critique (by an old friend)