Anzeige
Erschienen in:
2002 | OriginalPaper | Buchkapitel
Mechanical Verification of a Square Root Algorithm Using Taylor’s Theorem
verfasst von : Jun Sawada, Ruben Gamboa
Erschienen in: Formal Methods in Computer-Aided Design
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.