Next: Denormal Rounding Up: Rounding Previous: Sticky Rounding   Contents

# IEEE Rounding

The IEEE standard prescribes four rounding modes: “round to nearest” (near), “round toward 0” (trunc), “round toward +INFINITY”, and “round toward -INFINITY”. The last two are formalized here by the functions inf and minf.

Definition 5.5.1   (inf) For all and ,

inf

(inf-lower-bound) For all and ,

inf

PROOF: If , then

inf

if , then

inf

Definition 5.5.2   (minf) For all and ,

minf

(minf-upper-bound) For all and ,

minf

PROOF: If , then

minf

if , then

inf

In this section, we collect a set of general results that pertain to all of the IEEE rounding modes, most of which are essentially restatements of lemmas that are proved in earlier sections. Since these results also hold for two of the other modes that we have discussed, away and , we shall state them as generally as possible. For this purpose, we define a common rounding mode to be any of the six, i.e., trunc, away, near, , inf, or minf.

(rnd-choice) Let be a common rounding mode. For all and , either

or

PROOF: This is an immediate consequence of Definitions 5.3.1, 5.3.2, 5.5.1, and 5.5.2

Most of following results are consequences of Lemma 5.5.3 and the corresponding lemmas pertaining to trunc and away.

(sgn-rnd) Let and . Let be a common rounding mode. If , then

PROOF: See Lemmas 5.1.2 and 5.2.2

Note that inf and minf do not share the oddness property held by the other modes. A generalization is given by the following lemma.

(rnd-minus) Let be a common rounding mode and let

For all and ,

PROOF: Suppose, for example, that    inf and . Then since ,

inf

The other cases are handled similarly.

(rnd-exactp-a) Let be a common rounding mode. For all and , is -exact.

PROOF: See Lemmas 5.1.9 and 5.2.11

(rnd-exactp-b) Let and and let be a common rounding mode. If and x is -exact, then

PROOF: See Lemmas 5.1.11 and 5.2.13

(rnd-exactp-c,rnd-exactp-d) Let , , and , , and let be a common rounding mode. Suppose is -exact.

 (a) If , then . (b) If , then .

PROOF: See Lemmas 5.1.12 and 5.2.14

(rnd<=away, rnd>=trunc) Let and and let be a common rounding mode. If , then

PROOF: This is an immediate consequence of Lemmas 5.1.5 and 5.2.5:

(rnd-diff) Let , , , and let be a common rounding mode. Then

PROOF: See Lemmas 5.1.8 and 5.2.7

(expo-rnd) Let be a common rounding mode. For all and , if , then

PROOF: See Lemmas 5.1.6 and 5.2.10

(rnd-monotone) Let , , and . Let be a common rounding mode. If and , then

PROOF: The modes trunc, away, near, and are covered by Lemmas 5.1.13, 5.2.15, 5.3.13, and 5.3.30. For the modes inf and minf, we may assume, using Lemma 5.5.4, that and are either both positive or both negative. It follows that either

or

(rnd-shift) Let be a common rounding mode. For all , , and ,

PROOF: The modes trunc, away, near, and are covered by Lemmas 5.1.4, 5.2.4, 5.3.8, and 5.3.20. For the modes inf and minf, we may assume, using Lemma 5.5.5, that , in which case

infinf

and

minfminf

(plus-rnd) Let be a common rounding mode, , , and with and . Let and . If is -exact, then

PROOF: See Lemmas 5.1.16 and 5.2.19

(rnd-sticky) Let be a common rounding mode, , , and . If and , then

PROOF: The modes trunc and away are handled by Lemma 5.4.9; near and are covered by Lemma 5.4.10; inf and minf are reduced to trunc and away by Lemma 5.4.1

For the sake of simplicity, our main result pertaining to constant injection is formulated in the context of bit vector rounding.

(rnd-const-thm) Let be a common rounding mode, , , and with . Then

where

and

PROOF: For the modes away and inf, the identity follows from Lemma 5.2.22, with , and Lemma 4.2.7. For near and , it reduces to Lemma 5.3.34. For trunc and minf, the lemma is trivial.

Our final result provides an alternative to Lemma 5.5.16 as an implementation of rounding.

(roundup-thm) Let be a common rounding mode, , and with . If any of the following conditions holds, then    fp :
(1) and

(2) , , and either
(a) is not -exact or
(b)

(3)    inf or and is not -exact.

In all other cases, .

PROOF: Suppose first that is -exact. By Lemma 4.2.10, , and it follows from Lemma 2.3.12 that

Consequently, none of the conditions (1)-(3) holds, and by Lemma 5.5.7,

Therefore, we may assume that is not -exact. Note that by Lemma 5.2.16,

The cases ,    minf , , and    inf now follow trivially.

We turn to the cases and . Let

and

Since , Lemma 1.2.7 implies

By Lemmas 2.2.11 and 2.2.19,

Therefore,

Using Lemma 2.3.13, we may further reduce this to

By Lemma 2.2.1,

This leads to the following observations:

(i)
if and only if .

(ii)
if and only if and , and according to Lemma 4.2.10, the latter condition holds if and only if is not -exact.

Referring to Definition 5.3.2, we see that (i) is sufficient to complete the proof for the case .

For the case , it is clear from Definition 5.3.1 and (i) and (ii) above that we need only show that is odd if and only if . But according to Lemmas 2.3.2 and 2.3.12,

Next: Denormal Rounding Up: Rounding Previous: Sticky Rounding   Contents
David Russinoff 2007-01-02