Subscribe

Issue No.05 - May (2013 vol.62)

pp: 900-913

D. M. Russinoff , Intel Corp., Austin, TX, USA

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2012.40

ABSTRACT

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.40REFERENCES

- [1] ACL2 Web Site, www.cs.utexas.edu/users/mooreacl2, 2012.
- [2] E.D. Atkins, "Higher-Radix Division Using Estimates of the Divisor and Partial Remainder,"
IEEE Trans. Computers, vol. 17, no. 10, pp. 925-934, Oct. 1968.- [3] L. Ciminiera and P. Montuschi, "Higher Radix Square Rooting,"
IEEE Trans. Computers, vol. 39, no. 10, pp. 1220-1231, Oct. 1990.- [4] M.E. Clarke, S.M. German, and X. Zhou, "Verifying the SRT Division Algorithm Using Theorem Proving Techniques,"
Formal Methods in System Design, vol. 14, no. 1, pp. 7-44, Jan. 1999.- [5] J. Coke et al., "Improvements in the Intel Core 2 Penryn Processor Family Architecture and Microarchitecture,"
Intel Technology J., vol. 12, no. 3, Oct. 2008.- [6] J. Fandrianto, "Algorithm for High Speed Shared Radix 8 Division and Radix 8 Square Root,"
Proc. IEEE Ninth Symp. Computer Arithmetic, 1989.- [7] G. Gerwig, H. Wetter, E.M. Schwarz, J. Haess, C.A. Krygowski, B.M. Fleischer, and M. Kroener, "The IBM eServer z990 Floating-Point Unit,"
IBM J. Research and Development, vol. 48, nos. 3/4, pp. 311-322, 2004.- [8] F.R. Hobson and M.W. Fraser, "An Efficient Maximum-Redundancy Radix-8 SRT Division and Square-Root Method,"
IEEE J. Solid State Circuits, vol. 30, no. 1, pp. 29-38, Jan. 1995.- [9] D. Kapur and M. Subramaniam, "Mechanizing Verification of Arithmetic Circuits: SRT Division,"
Proc. 17th Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS-17), pp. 103-122, Dec. 1997.- [10] P. Kornerup, "Digit Selection for SRT Division and Square Root,"
IEEE Trans. Computers, vol. 54, no. 3, pp. 294-303, Mar. 2005.- [11] S. Oberman and M. Flynn, "Minimizing the Complexity of SRT Tables,"
IEEE Trans. Very Large Scale Integration Systems, vol. 6, no. 1, pp. 141-149, Mar. 1998.- [12] B. Parhami, "Tight Upper Bounds on the Minimum Precision of the Divisor and the Partial Remainder in High-Radix Division,"
IEEE Trans. Computers, vol. 52, no. 11, pp. 1509-1514, Nov. 2003.- [13] V. Pratt, "Anatomy of the Pentium Bug,"
Proc. Sixth Int'l Joint Conf. CAAP/FASE on Theory and Practice of Software Development (TAPSOFT '95), May 1995.- [14] H. Ruess, N. Shankar, and M.K. Srivas, "Modular Verification of SRT Division,"
Formal Methods in System Design, vol. 14, no. 1, pp. 45-73, Jan. 1999.- [15] D.M. Russinoff, "Mechanical Verification of a Commercial SRT Divider,"
Design and Verification of Microprocessor Systems for High-Assurance Applications, D.S. Hardin, Springer, www.russinoff. com/paperssrt.html, 2010.- [16] G.S. Taylor, "Compatible Hardware for Division and Square Root,"
Proc. IEEE Fifth Symp. Computer Arithmetic, 1981. |