Formal verification of floating point trigonometric functions

John Harrison

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


We have formal verified a number of algorithms for evaluating transcendental functions in double-extended precision floating point arithmetic in the Intel (R) IA-64 architecture. These algorithms are used in the Itanium (TM) processor to prove compatibility with IA-32 (x86) hardware transcendentals, and similar ones are used in mathematical software libraries. In this paper we describe in some depth the formal verification of the sin and cos functions, including the initial range reduction step. This illustrates the different facets of verification in this field, covering both pure mathematics and the detailed analysis of floating point rounding.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:39
Start Conference Manager
Conference Systems