Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd - Archive ouverte HAL Access content directly
Journal Articles IEEE Transactions on Computers Year : 2008

Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd

(1) , (2)
1
2
Sylvie Boldo
Guillaume Melquiond

Abstract

Rounding to odd is a non-standard rounding on floating-point 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 multiply-and-add operator. We also present an iterative algorithm for computing the correctly rounded sum of a set floating-point numbers under mild assumptions. A variation on both previous algorithms is the correctly rounded sum of any three floating-point 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.
Fichier principal
Vignette du fichier
odd-rounding.pdf (282.56 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00080427 , version 1 (16-06-2006)
inria-00080427 , version 2 (10-11-2010)

Identifiers

Cite

Sylvie Boldo, Guillaume Melquiond. Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd. IEEE Transactions on Computers, 2008, 57 (4), pp.462-471. ⟨10.1109/TC.2007.70819⟩. ⟨inria-00080427v2⟩
2716 View
5853 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More