Emulating Round-to-Nearest Ties-to-Zero Augmented Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic

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.

Automated summary

The 2019 version of the IEEE 754 Standard recommends new augmented operations for binary formats, utilizing a new rounding direction: round-to-nearest ties-to-zero. These operations can be implemented using currently available operations, with a partial formal proof of correctness using round-to-nearest ties-to-even.