Emulating round-to-nearest-ties-to-zero "augmented" floating-point operations using round-to-nearest-ties-to-even arithmetic

Sylvie Boldo (1, 2) , Christoph Q. Lauter (3) , Jean-Michel Muller (4, 5, 6)

1 LRI - Laboratoire de Recherche en Informatique
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
3 University of Alaska [Anchorage]
4 Université de Lyon
5 ARIC - Arithmetic and Computing
6 LIP - Laboratoire de l'Informatique du Parallélisme

The 2019 version of the IEEE 754 Standard for Floating-Point Arithmetic recommends that new “augmented” operations should be provided for the binary formats. These operations use a new “rounding direction”: round to nearest ties-to-zero. We show how they can be implemented using the currently available operations, using round-to-nearest ties-to-even with a partial formal proof of correctness.

Keywords: Floating-point arithmetic; Numerical reproducibility; Rounding error analysis; Rounding mode; Error-free transforms; Formal proof

Domains: Other [cs.OH]; Computer Arithmetic

Sylvie Boldo, Christoph Q. Lauter, Jean-Michel Muller. Emulating round-to-nearest-ties-to-zero "augmented" floating-point operations using round-to-nearest-ties-to-even arithmetic. 2019. ⟨hal-02137968v3⟩