Application of Theorem Proving to Arithmetic Circuits

  • 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