We present a proof of correctness of a commercial implementation of the Sweeney-Robertson-Tocher (SRT) division algorithm, namely the integer divider of the AMD processor code-named "Llano". The register-transfer logic (RTL) design of the divider and its behavioral specification are both formalized in the ACL2 logic; the proof has been formally checked by the ACL2 prover. The complexity of the problem is managed by modeling the design at successively lower levels of abstraction, beginning with the SRT algorithm and ending with the RTL module. This approach is contrasted with earlier published work on this problem, which addresses only the high-level algorithm.
Full paper: ps,