Formal verification of IA-64 division and square root

IA-64 is a new 64-bit computer architecture jointly developed by Hewlett-Packard and Intel, and the forthcoming Merced chip from Intel will be its first silicon implementation. Division and square root in IA-64 are intended to be implemented in software, using approximation instructions and standard floating-point operations provided. A number of recommended code sequences (for calling as subroutines or inlining by compilers) are provided. We discuss how we used HOL Light to verify that these always deliver IEEE-correct results.

LS Home page or Talks in 1999/2000