- ACL2, successor to Nqtm (Boyer-Moore Theorem Prover), used at AMD to
formally verify floating point units
- First used by Moore et al. to check the proof of correctness
of the Kernel of the AMD 5k86 floating point division algorithm
- mechanically checked proof of correctness of the kernel
-
Recently used to verify the RTL of the K7 Floating
Point Unit
- RTL primitives are logical operations on bit vectors
- Developed theory of bit vectors to prove RTL correct with respect
to the more abstract IEEE standard
|
