Mechanical verification of a square root algorithm using taylor’s theorem

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 proofrequires the analysis on the approximation error ofCheb yshev 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 ofnon-standard analysis, as implemented in ACL2(r). Since a Taylor polynomial has less accuracy than the Chebyshev polynomial ofthe same degree, we used hundreds ofT aylor polynomial generated by ACL2(r) to evaluate the error ofa Chebyshev polynomial.