Emulating Round-to-Nearest Ties-to-Zero “Augmented” Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic
Sylvie Boldo, Christoph Lauter, Jean‐Michel Muller · IEEE Transactions on Computers · 2020
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-nearestties-to-zero. We show how they can be implemented using the currently available operations, using round-to-nearestties-to-evenwith a partial formal proof of correctness.