Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
Article No.: 9, Pages 1 - 22
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.
References
[1]
Behzad Akbarpour and Lawrence C. Paulson. 2008. MetiTarski: An automatic prover for the elementary functions. In International Conference on Intelligent Computer Mathematics. Springer, 217–231.
[2]
Behzad Akbarpour and Lawrence C. Paulson. 2009. Applications of MetiTarski in the verification of control and hybrid systems. In Hybrid Systems: Computation and Control (LNCS 5469), Rupak Majumdar and Paulo Tabuada (Eds.). Springer, 1–15.
[3]
Behzad Akbarpour and Lawrence Charles Paulson. 2010. MetiTarski: An automatic theorem prover for real-valued special functions. Journal of Automated Reasoning 44, 3 (2010), 175–205.
[4]
Ray Andraka. 1998. A survey of CORDIC algorithms for FPGA based computers. In Proceedings of the 1998 ACM/SIGDA 6th International Symposium on Field Programmable Gate Arrays. 191–200.
[5]
J.-C. Bajard, Sylvanus Kla, and J.-M. Muller. 1994. BKM: A new hardware algorithm for complex elementary functions. IEEE Trans. Comput. 43, 8 (1994), 955–963.
[6]
Sylvie Boldo and Jean-Christophe Filliâtre. 2007. Formal verification of floating-point programs. In 18th IEEE Symposium on Computer Arithmetic. IEEE, 187–194.
[7]
Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. 2009. Combining Coq and Gappa for certifying floating-point programs. In International Conference on Intelligent Computer Mathematics. Springer, 59–74.
[8]
Sylvie Boldo and Guillaume Melquiond. 2011. Flocq: A unified library for proving floating-point algorithms in Coq. In 20th IEEE Symposium on Computer Arithmetic (ARITH’11). IEEE, 243–252.
[9]
Nicolas Brisebarre and Sylvain Chevillard. 2007. Efficient polynomial L-approximations. In 18th IEEE Symposium on Computer Arithmetic (ARITH’07). IEEE, 169–176.
[10]
Christopher W. Brown. 2003. QEPCAD B: A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin 37, 4 (2003), 97–108.
[11]
D. Chen, L. Han, Y. Choi, and S. Ko. 2012. Improved decimal floating-point logarithmic converter based on selection by rounding. IEEE Trans. Comput. 61, 5 (2012), 607–621.
[12]
D. Chen, Y. Zhang, Y. Choi, M. H. Lee, and S. Ko. 2009. A 32-bit decimal floating-point logarithmic converter. In 19th IEEE Symposium on Computer Arithmetic. IEEE, 195–203.
[13]
S. Chevillard, M. Joldeş, and C. Lauter. 2010. Sollya: An environment for the development of numerical codes. In Mathematical Software (ICMS’10)(Lecture Notes in Computer Science, Vol. 6327), K. Fukuda, J. van der Hoeven, M. Joswig, and N. Takayama (Eds.). Springer, Heidelberg, Germany, 28–31.
[14]
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. 2017. Satisfiability modulo transcendental functions via incremental linearization. In International Conference on Automated Deduction. Springer, 95–113.
[15]
William James Cody. 1980. Software Manual for the Elementary Functions (Prentice-Hall Series in Computational Mathematics). Prentice-Hall, Inc.
[16]
Marc Daumas, David Lester, and César Munoz. 2008. Verified real number calculations: A library for interval arithmetic. IEEE Trans. Comput. 58, 2 (2008), 226–237.
[17]
Marc Daumas and Guillaume Melquiond. 2010. Certification of bounds on expressions involving rounded operators. ACM Transactions on Mathematical Software (TOMS) 37, 1 (2010), 2.
[18]
Marc Daumas, Laurence Rideau, and Laurent Théry. 2001. A generic library for floating-point numbers and its application to exact computing. In International Conference on Theorem Proving in Higher Order Logics. Springer, 169–184.
[19]
Florent de Dinechin, Mioara Joldes, and Bogdan Pasca. 2010. Automatic generation of polynomial-based hardware architectures for function evaluation. In Application-specific Systems, Architectures and Processors. IEEE, 216–222.
[20]
F. de Dinechin, C. Lauter, and G. Melquiond. 2011. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Trans. Comput. 60, 2 (2011), 242–253.
[21]
Florent De Dinechin, Christoph Quirin Lauter, and Guillaume Melquiond. 2006. Assisted verification of elementary functions using Gappa. In ACM Symposium on Applied Computing. ACM, 1318–1322.
[22]
Florent de Dinechin and Bogdan Pasca. 2011. Designing custom arithmetic data paths with FloPoCo. IEEE Design & Test of Computers 28, 4 (July 2011), 18–27.
[23]
Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340.
[24]
William Denman, Behzad Akbarpour, Sofiene Tahar, Mohamed H. Zaki, and Lawrence C. Paulson. 2009. Formal verification of analog designs using MetiTarski. In Formal Methods in Computer-Aided Design, 2009 (FMCAD’09). IEEE, 93–100.
[25]
Laurent Fousse, Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, and Paul Zimmermann. 2007. MPFR: A multiple-precision binary floating-point library with correct rounding. ACM Transactions on Mathematical Software (TOMS) 33, 2 (2007), 13.
[26]
Raymond E. Fowkes. 1993. Hardware efficient algorithms for trigonometric functions. IEEE Trans. Comput. 42, 2 (1993), 235–239.
[27]
Shmuel Gal. 1991. An accurate elementary mathematical library for the IEEE floating point standard. ACM Transactions on Mathematical Software (TOMS) 17, 1 (1991), 26–45.
[28]
Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT solver for nonlinear theories over the reals. In International Conference on Automated Deduction. Springer, 208–214.
[29]
David Goldberg. 1991. What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys (CSUR) 23, 1 (1991), 5–48.
[30]
David Harris. 2001. A powering unit for an OpenGL lighting engine. In Conference Record of 35th Asilomar Conference on Signals, Systems and Computers (Cat. No. 01CH37256), Vol. 2. IEEE, 1641–1645.
[31]
John Harrison. 1997. Floating point verification in HOL Light: The exponential function. In International Conference on Algebraic Methodology and Software Technology. Springer, 246–260.
[32]
John Harrison. 1999. A machine-checked theory of floating point arithmetic. In International Conference on Theorem Proving in Higher Order Logics. Springer, 113–130.
[33]
John Harrison. 2006. Floating-point verification using theorem proving. In International School on Formal Methods for the Design of Computer, Communication and Software Systems. Springer, 211–242.
[34]
J. Harrison. 2009. Decimal transcendentals via binary. In 19th IEEE Symposium on Computer Arithmetic. IEEE, 187–194.
[35]
John Harrison, Ted Kubaska, Shane Story, and Ping Tak Peter Tang. 1999. The computation of transcendental functions on the IA-64 architecture. In Intel Technology Journal. Citeseer.
[36]
Wolfram Research, Inc.2021. Mathematica, Version 12.1. https://www.wolfram.com/mathematica.
[37]
Christian Jacobi and Christoph Berg. 2005. Formal verification of the VAMP floating point unit. Formal Methods in System Design 26, 3 (2005), 227–266.
[38]
Wonyeol Lee, Rahul Sharma, and Alex Aiken. 2016. Verifying bit-manipulations of floating-point. ACM SIGPLAN Notices 51, 6 (2016), 70–84.
[39]
Joe Leslie-Hurd. 2007. Metis Theorem Prover. http://www.gilith.com/software/metis/.
[40]
David M. Lewis. 1995. 114 MFLOPS logarithmic number system arithmetic unit for DSP applications. IEEE Journal of Solid-State Circuits 30, 12 (1995), 1547–1553.
[41]
Catherine Daramy, David Defour, Florent De Dinechin, and Jean-Michel Muller. 2003. CR-LIBM: a correctly rounded elementary function library. In Advanced Signal Processing Algorithms, Architectures, and Implementations XIII. Vol. 5205. DOI:
[42]
Michel Ludwig and Uwe Waldmann. 2007. An extension of the Knuth-Bendix ordering with LPO-like properties. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, 348–362.
[43]
Érik Martin-Dorel and Guillaume Melquiond. 2016. Proving tight bounds on univariate expressions with elementary functions in Coq. Journal of Automated Reasoning 57, 3 (2016), 187–217.
[44]
Guillaume Melquiond. 2012. Floating-point arithmetic in the Coq system. Information and Computation 216 (2012), 14–23.
[45]
Antoine Miné. 2013. Abstract domains for bit-level machine integer and floating-point operations. In ATx’12/WInG’12: Workshop on Invariant Generation(EPiC Series in Computing, Vol. 17), Jacques Fleuriot, Peter Höfner, Annabelle McIver, and Alan Smaill (Eds.). 55–70.
[46]
J. Strother Moore, Tom Lynch, and Matt Kaufmann. 1996. A mechanically checked proof of the correctness of the kernel of the AMD5k86 floating point division algorithm. http://devil.ece.utexas.edu.
[47]
Jean-Michel Muller, Nicolas Brisebarre, Florent De Dinechin, Claude-Pierre Jeannerod, Vincent Lefevre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. 2010. Handbook of Floating-Point Arithmetic. Springer.
[48]
J. Pineiro, M. D. Ercegovac, and J. D. Bruguera. 2002. High-radix logarithm with selection by rounding. In Proceedings of the IEEE International Conference on Application- Specific Systems, Architectures, and Processors. IEEE, 101–110.
[49]
J.-A. Pineiro, Milos D. Ercegovac, and Javier D. Bruguera. 2004. Algorithm and architecture for logarithm, exponential, and powering computation. IEEE Trans. Comput. 53, 9 (2004), 1085–1096.
[50]
J.-A. Pineiro, Stuart F. Oberman, J.-M. Muller, and Javier D. Bruguera. 2005. High-speed function approximation using a minimax quadratic interpolator. IEEE Trans. Comput. 54, 3 (2005), 304–318.
[51]
Vaughan Pratt. 1995. Anatomy of the Pentium bug. In Colloquium on Trees in Algebra and Programming. Springer, 97–107.
[52]
David M. Russinoff. 1998. A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7™ processor. LMS Journal of Computation and Mathematics 1 (1998), 148–200.
[53]
M. Schulte and E. Swartzlander. 1993. Exact rounding of certain elementary functions. In Proceedings of IEEE 11th Symposium on Computer Arithmetic. IEEE, 138–145.
[54]
Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamarić, and Ganesh Gopalakrishnan. 2018. Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. ACM Transactions on Programming Languages and Systems (TOPLAS) 41, 1 (2018), 1–39.
[55]
Shane Story and Ping Tak Peter Tang. 1999. New algorithms for improved transcendental functions on IA-64. In Proceedings of the 14th IEEE Symposium on Computer Arithmetic. IEEE, 4–11.
[56]
Antonio G. M. Strollo, Davide De Caro, and Nicola Petra. 2011. Elementary functions hardware implementation using constrained piecewise-polynomial approximations. IEEE Trans. Comput. 60, 3 (2011), 418–432.
[57]
Ping Tak Peter Tang. 1991. Table-lookup algorithms for elementary functions and their error analysis. In 10th IEEE Symposium on Computer Arithmetic. IEEE, 232–236.
[58]
L. Veidinger. 1960. On the numerical determination of the best approximations in the Chebyshev sense. Numer. Math. 2, 1 (1960), 99–105.
[59]
Jack Volder. 1959. The CORDIC computing technique. In Papers Presented at the March 3–5, 1959, Western Joint Computer Conference. 257–261.
[60]
J. S. Walther. 1971. A unified algorithm for elementary functions. In Proceedings of the May 18–20, 1971, Spring Joint Computer Conference (AFIPS’71 (Spring)). Association for Computing Machinery, New York, NY, 379–385.
Index Terms
- Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
Recommendations
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification
ICCD '95: Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and ProcessorsThe effectiveness of hardware verification techniques has increased markedly in the past decade. As hardware verification techniques become increasingly powerful the idea of transitioning verification technology to industry can be taken seriously. ...
Interactive verification of concurrent systems using symbolic execution
Practical Aspects of Automated ReasoningThis paper presents an interactive proof method for the verification of temporal properties of concurrent systems based on symbolic execution. Symbolic execution is a well known and very intuitive strategy for the verification of sequential programs. We ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2022
113 pages
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 19 September 2022
Online AM: 13 June 2022
Accepted: 30 May 2022
Received: 18 November 2020
Published in FAC Volume 34, Issue 2
Check for updates
Author Tags
Qualifiers
- Research-article
- Refereed
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 1,348Total Downloads
- Downloads (Last 12 months)486
- Downloads (Last 6 weeks)38
Reflects downloads up to 13 Dec 2024
Other Metrics
Citations
View Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderFull Text
View this article in Full Text.
Full TextLogin options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in