Abstract
The IBM Power4™ processor uses Chebyshev polynomials to calculate square root. We formally verified the correctness of this algorithm using the ACL2(r) theorem prover. The proof requires the analysis on the approximation error of Chebyshev polynomials. This is done by proving Taylor’s theorem, and then analyzing the Chebyshev polynomial using Taylor polynomials. Taylor’s theorem is proven by way of non-standard analysis, as implemented in ACL2(r). Since a Taylor polynomial has less accuracy than the Chebyshev polynomial of the same degree, we used hundreds of Taylor polynomial generated by ACL2(r) to evaluate the error of a Chebyshev polynomial.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. D. Aagaard, R. B. Jones, R. Kaivola, K. R. Kohatsu, and C.-J. H. Seger. Formal verification of iterative algorithms in microprocessors. Proceedings Design Automation Conference (DAC 2000), pages 201–206, 2000.
R. C. Agarwal, F. G. Gustavson, and M. S. Schmookler. Series approximation methods for divide and square root in the Power3 processor. In Proceedings of the 14th IEEE Symposium on Computer Arithmetic, pages 116–123, 1999.
W. Fulks. Advanced Calculus: an introduction to analysis. John Wiley & Sons, third edition, 1978.
R. Gamboa. Mechanically Verifying Real-Valued Algorithms in ACL2. PhD thesis, University of Texas at Austin, 1999.
R. Gamboa. The correctness of the Fast Fourier Trasnform: A structured proof in ACL2. Formal Methods in System Design, 20:91–106, January 2002.
R. Gamboa and M. Kaufmann. Nonstandard analysis in ACL2. Journal of Automated Reasoning, 27(4):323–351, November 2001.
R. Gamboa and B. Middleton. Taylor’s formula with remainder. In Proceedings of the Third International Workshop of the ACL2 Theorem Prover and its Applications (ACL2-2002), 2002.
J. Harrison. Verifying the accuracy of polynomial approximations in HOL. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs’97, volume 1275 of LNCS, pages 137–152. Springer-Verlag, 1997.
J. Harrison. Formal verification of floating point trigonometric functions. In W. A. Hunt and S. D. Johnson, editors, Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000, volume 1954 of LNCS, pages 217–233. Springer-Verlag, 2000.
Institute of Electrical and Electronic Engineers. IEEE Standard for Binary Floating-Point Arithmetic. ANSI/IEEE Std 754-1985.
M. Kaufmann. Modular proof: The fundamental theorem of calculus. In M. Kaufmann, P. Manolios, and J. S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, chapter 6. Kluwer Academic Press, 2000.
M. Kaufmann and J. S. Moore. ACL2: An industrial strength version of nqthm. In Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23–34. IEEE Computer Society Press, June 1996.
E. Nelson. On-line books: Internal set theory. Available on the world-wide web at http://www.math.princeton.edu/~nelson/books.html.
E. Nelson. Internal set theory. Bulletin of the American Mathematical Society, 83:1165–1198, 1977.
J. O’Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, Q1, Feb. 1999.
A. Robert. Non-Standard Analysis. John Wiley, 1988.
A. Robinson. Model theory and non-standard arithmetic, infinitistic methods. In Symposium on Foundations of Mathematics, 1959.
D. Russinoff. A Mechanically Checked Proof of Correctness of the AMDK5 Floating-Point Square Root Microcode. Formal Methods in System Design, 14(1), 1999.
D. M. Russinoff. A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division, and Square Root Algorithm of the AMDK7 Processor. J. Comput. Math. (UK), 1, 1998.
J. Sawada. ACL2 computed hints: Extension and practice. In ACL2 Workshop 2000 Proceedings, Part A. The University of Texas at Austin, Department of Computer Sciences, Technical Report TR-00-29, Nov. 2000.
J. Sawada. Formal verification of divide and square algorithms using series calculation. Technical Report RC22444, IBM, May 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sawada, J., Gamboa, R. (2002). Mechanical Verification of a Square Root Algorithm Using Taylor’s Theorem. In: Aagaard, M.D., O’Leary, J.W. (eds) Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, vol 2517. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36126-X_17
Download citation
DOI: https://doi.org/10.1007/3-540-36126-X_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00116-4
Online ISBN: 978-3-540-36126-8
eBook Packages: Springer Book Archive