A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 TM processor
David M. Russinoff
Abstract: 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.
|
