This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables
May 2013 (vol. 62 no. 5)
pp. 900-913
D. M. Russinoff, Intel Corp., Austin, TX, USA
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.
Index Terms:
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
Citation:
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
Usage of this product signifies your acceptance of the Terms of Use.