The Community for Technology Leaders
Green Image
Issue No. 08 - August (2009 vol. 58)
ISSN: 0018-9340
pp: 1139-1145
Ren-Cang Li , University of Texas at Arlington, Arlington
Marc Daumas , ELIAUS, UPVD, Perpignan
Sylvie Boldo , INRIA Saclay, Orsay
ABSTRACT
The Cody and Waite argument reduction technique works perfectly for reasonably large arguments, but as the input grows, there are no bits left to approximate the constant with enough accuracy. Under mild assumptions, we show that the result computed with a fused multiply-add provides a fully accurate result for many possible values of the input with a constant almost accurate to the full working precision. We also present an algorithm for a fully accurate second reduction step to reach full double accuracy (all the significand bits of two numbers are accurate) even in the worst cases of argument reduction. Our work recalls the common algorithms and presents proofs of correctness. All the proofs are formally verified using the Coq automatic proof checker.
INDEX TERMS
Argument reduction, fma, formal proof, Coq.
CITATION
Ren-Cang Li, Marc Daumas, Sylvie Boldo, "Formally Verified Argument Reduction with a Fused Multiply-Add", IEEE Transactions on Computers, vol. 58, no. , pp. 1139-1145, August 2009, doi:10.1109/TC.2008.216
98 ms
(Ver 3.1 (10032016))