Subscribe
Issue No.04  April (2008 vol.57)
pp: 462471
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2007.70819
ABSTRACT
Rounding to odd is a nonstandard rounding on floatingpoint numbers. By using it for some intermediate values instead of rounding to nearest, correctly rounded results can be obtained at the end of computations. We present an algorithm to emulate the fused multiplyandadd operator. We also present an iterative algorithm for computing the correctly rounded sum of a set floatingpoint numbers under mild assumptions. A variation on both previous algorithms is the correctly rounded sum of any three floatingpoint numbers. This leads to efficient implementations, even when this rounding is not available. In order to guarantee the correctness of these properties and algorithms, we formally proved them using the Coq proof checker.
INDEX TERMS
Computer arithmetic, Verification
CITATION
Sylvie Boldo, Guillaume Melquiond, "Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd", IEEE Transactions on Computers, vol.57, no. 4, pp. 462471, April 2008, doi:10.1109/TC.2007.70819
REFERENCES
