We discuss the verification of algorithms for computing common transcendental functions such as ln and sin in floating point arithmetic. Our method relates the floating point operations to their abstract real number counterparts; we discuss several different ways of doing this. The algorithms are expressed in a general imperative language and verified according to a formal semantics. Apart from being a straightforward `pseudocode', this language can be embedded as a simple subset either of programming languages like C or hardware description languages like Verilog. Thus we allow the target implementation to be either in software or hardware. All verification, including the embedding of the programming language semantics, is done in HOL Light, a new version of the HOL theorem prover.
We focus our attention on two basic algorithms, following through inside HOL some error analyses in the literature and some of our own. Both these algorithms are of current interest, and some versions of them are used in real contemporary computer systems. Moreover, the two algorithms and their implementation assumptions are quite different, emphasizing the flexibility of our approach. The first algorithm relies on large lookup tables of precomputed results together with the use of a low-order polynomial approximation to interpolate between them. The subsidiary calculations are assumed to be performed using IEEE-754 standard arithmetic, which we formalize. The second algorithm is based on the CORDIC technique, which successively approximates a function using only efficient shifts and adds. Our error analysis here assumes the use of an internal fixed-point format for the main loop.
This talk will focus on the general issues rather than the low-level technical details.