Formal Verification of Transcendental Fixed and Floating Point Algorithms using an Automatic Theorem Prover
Open Access
- 13 June 2022
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 34 (2)
- https://doi.org/10.1145/3543670
Abstract
We present a method for formal verification of transcendental hardware and software algorithms that scales to higher precision without suffering an exponential growth in runtimes. A class of implementations using piecewise polynomial approximation to compute the result is verified using MetiTarski, an automated theorem prover, which verifies a range of inputs for each call. The method was applied to commercial implementations from Cadence Design Systems with significant runtime gains over exhaustive testing methods and was successful in proving that the expected accuracy of one implementation was overly optimistic. Reproducing the verification of a sine implementation in software, previously done using an alternative theorem proving technique, demonstrates that the MetiTarski approach is a viable competitor. Verification of a 52 bit implementation of the square root function highlights the method’s high precision capabilities.Keywords
This publication has 31 references indexed in Scilit:
- Certification of bounds on expressions involving rounded operatorsACM Transactions on Mathematical Software, 2010
- MPFRACM Transactions on Mathematical Software, 2007
- Algorithm and architecture for logarithm, exponential, and powering computationInternational Conference on Acoustics, Speech, and Signal Processing (ICASSP), 2004
- QEPCAD BACM SIGSAM Bulletin, 2003
- 114 MFLOPS logarithmic number system arithmetic unit for DSP applicationsIEEE Journal of Solid-State Circuits, 1995
- BKM: a new hardware algorithm for complex elementary functionsInternational Conference on Acoustics, Speech, and Signal Processing (ICASSP), 1994
- Hardware efficient algorithms for trigonometric functionsInternational Conference on Acoustics, Speech, and Signal Processing (ICASSP), 1993
- What every computer scientist should know about floating-point arithmeticACM Computing Surveys, 1991
- An accurate elementary mathematical library for the IEEE floating point standardACM Transactions on Mathematical Software, 1991
- On the numerical determination of the best approximations in the Chebyshev senseNumerische Mathematik, 1960