Issue No.05 - May (2013 vol.62)
D. M. Russinoff , Intel Corp., Austin, TX, USA
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2012.40
We present a comprehensive, self-contained, and mechanically verified proof of correctness of a maximally redundant SRT design for floating-point division and square root extraction, supported by verified procedures that 1) test the admissibility of a proposed digit selection table, 2) determine the minimal dimensions of an admissible table for a given arbitrary radix, and 3) generate these tables. For square root extraction, we also provide a verified procedure for generating an initial approximation that meets the accuracy requirement of the algorithm and ensures that the digit selection index derived from successive partial roots remains static throughout the computation. A radix-8 instantiation of these algorithms has been implemented in the floating-point unit of the AMD processor code-named Steamroller. To ensure their correctness, all of our results and procedures have been formalized and mechanically checked by the ACL2 prover. We present evidence of the value of this approach by comparing it to that of a more conventional published paper that reports similar results, which are shown to be fatally flawed.
microprocessor chips, floating point arithmetic, formal verification, ACL2 prover, formal verification, SRT quotient, square root digit selection tables, maximally redundant SRT design, floating-point division, square root extraction, arbitrary radix, digit selection index, partial roots, radix-8 instantiation, floating-point unit, AMD processor code, Steamroller, Approximation methods, Approximation algorithms, Redundancy, Indexes, Reliability engineering, Algorithm design and analysis, formal verification, Approximation methods, Approximation algorithms, Redundancy, Indexes, Reliability engineering, Algorithm design and analysis, SRT division, Interactive theorem proving
D. M. Russinoff, "Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables", IEEE Transactions on Computers, vol.62, no. 5, pp. 900-913, May 2013, doi:10.1109/TC.2012.40