# 6.5  IEEE Rounding

The IEEE standard prescribes four rounding modes: “round to nearest” (RNE), “round toward 0” ( ), “round toward ', and “round toward ”. The last two are formalized here by the functions RUP and RDN.

Definition 6.5.1   (rup) For all and ,

Definition 6.5.2   (rdn) For all and ,

The essential properties of these modes are given by the following two results.

PROOF: If , then

if , then

PROOF: If , then

if , then

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, RAZ 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., , RAZ, RNE, , RUP, or RDN.

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

or

PROOF: This is an immediate consequence of Definitions 6.3.1, 6.3.2, 6.5.1, and 6.5.2

Most of following results are consequences of Lemma 6.5.3 and the corresponding lemmas pertaining to and RAZ.

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

PROOF: See Lemmas 6.1.2 and 6.2.1

Note that RUP and RDN 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 and . Then since ,

The other cases are handled similarly.

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

PROOF: See Lemmas 6.1.9 and 6.2.11

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

PROOF: See Lemmas 6.1.10 and 6.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 6.1.11 and 6.2.14

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

PROOF: See Lemmas 6.1.8 and 6.2.7

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

PROOF: See Lemmas 6.1.6 and 6.2.10

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

PROOF: The modes , RAZ, RNE, and are covered by Lemmas 6.1.13, 6.2.17, 6.3.17, and 6.3.36. For the modes RUP and RDN, we may assume, using Lemma 6.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 , RAZ, RNE, and are covered by Lemmas 6.1.4, 6.2.3, 6.3.8, and 6.3.29. For the modes RUP and RDN, we may assume, using Lemma 6.5.5, that , in which case

and

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

PROOF: See Lemmas 6.1.16 and 6.2.21

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

PROOF: This is an immediate consequence of Lemmas 6.1.5 and 6.2.5:

If is not -exact and is sufficiently close to , then and round to the same value under any common rounding mode:

(rnd<equal, rnd>equal) Let , , and with and . Let be a common rounding mode. Assume that is not -exact. If either

(a) or

(b) ,

then .

PROOF: We show the proof of (a); (b) is similar.

By Lemma 6.5.11, we need only show that . We also note that by Lemmas 6.1.15 and 6.1.5,

Case 1: or

by Lemma 6.1.9, is -exact. By Lemma 6.1.11 (with and substituted for and ) and Definition 6.5.2,

Case 2: or

By Lemmas 6.2.20 and 6.2.18,

and by Lemma 6.2.15 and Definition 6.5.1,

Case 3: or

By Lemmas 6.2.5 and 6.2.18,

The claim follows from Lemmas 6.3.19 and 6.3.38

(rnd-near-equal) Let and with and . Assume that is not -exact. There exists , , such that for all and every common rounding mode , if , then .

PROOF: According to Lemma 6.5.15, this holds for

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

PROOF: The modes and RAZ are handled by Lemma 6.4.9; RNE and are covered by Lemma 6.4.10; RUP and RDN are reduced to and RAZ by Lemma 6.4.1

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

PROOF: This is a consequence of Lemmas 6.2.16, 6.3.12, 6.3.33, and 6.1.5

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 RAZ and RUP, the identity follows from Lemma 6.2.24, with , and Lemma 4.2.7. For RNE and RNA, it reduces to Lemmas 6.3.42 and 6.3.42. For and RDN, the lemma is trivial.

Another common implementation of rounding is provided by the following result. Suppose our objective is a correct -bit rounding (with respect to some common rounding mode) of a precise result , and that we have a bit-vector representation of . Then the desired result may be derived by rounding in the direction determined as follows:

(roundup-pos-thm) Let be a common rounding mode, , and . Assume that and . Let and .

(a) is -exact iff and .

(b) If any of the following conditions holds, then , and otherwise :

• or and at least one of the following is true:
• ;
• .

• and

• , , and at least one of the following is true:
• ;
• ;
• ;

PROOF: It is clear that . Definition 6.1.1,

and hence, by Lemma 6.1.15, .

(a) According to Lemmas 6.1.9 and 6.1.10, it suffices to show that iff either or . By Lemma 6.1.5,

and it is clear that iff either or . Now since is -exact, Lemma 4.2.5 implies that is -exact, and therefore, by Lemmas 6.1.9 and 6.1.20,

(b) Since and , we need only consider RAZ, RNE, and RNA.

Suppose . By Lemmas 6.2.18, 6.1.9, and 6.2.11,

Thus, iff . But we have shown that this holds iff and , as stated by the lemma.

For the remaining cases, RNE, and RNA, we refer directly to Definitions 6.3.1 and 6.3.2. Let

and

By Definition 2.0.1, . By Definition 6.1.1, and consequently and . By Lemma 6.1.20,

Thus,

By Lemma 6.1.8,

This leads to the following observations:
1. iff .
2. iff and , but by Lemma 6.1.20,

and hence iff and either or .
Referring to Definition 6.3.2, we see that (1) is sufficient to complete the proof for the case .

For the case , it is clear from Definition 6.3.1 and (1) and (2) above that we need only show that is even iff . But this is a consequence of the above equation

The final result of this section is a variation of Lemma 6.5.20 that allows us to compute the absolute value of a rounded result when the unrounded value is negative, given a signed integer (twos' complement) encoding of , i.e., , where .

(roundup-neg-thm) Let be a common rounding mode, , , and . Assume that and . Let , , and .

(a) If , then .

(b) is -exact iff and .

(c) If any of the following conditions holds, then , and otherwise :

• or ;

• or and both of the following are true:
• ;
• ;

• and at least one of the following is true:
• ;
• and ;

• and at least one of the following is true:
• and .

PROOF: Let . Then ,

and .

To prove (a), note that if , then since , we must have , , and .

For the proof of (b) and (c), by Lemmas 2.2.22 and 6.1.18, we have

Suppose first that . Then

and the lemma claims that (b)  is -exact and (c)  for all . Both claims follow trivially from Lemmas 4.2.15, 6.1.9, and 6.5.7.

In the remaining case, . By Lemma 4.2.16, is not -exact, and (b) follows. The claim (c) will be derived from Lemma 6.5.20. Note that if is defined as in Lemma 6.5.5, then

and (c) may be restated as follows:

If any of the following conditions holds, then , and otherwise :

• or ;

• or and both of the following are true:
• ;
• ;

• and at least one of the following is true:

• ;
• and ;

• and at least one of the following is true:
• and .

We invoke Lemma 6.5.20 with and substituted for and , respectively. This yields the following:

If any of the following conditions holds, then , and otherwise :

• or and at least one of the following is true:
• ;
• .

• and

• , , and at least one of the following is true:
• ;
• ;
• ;

We must show that implies .

Suppose . Then and by Lemma 1.1.7,

and we may replace with in . Furthermore, , which implies , and the claim follows trivially from .

In the final case, and . Thus, and . Since

. Since

, which implies . Lemma 6.1.18 implies , and again we may replace with in . Furthermore,

If , then and

which implies and . On the other hand, if , then , which implies

and

In either case, again follows easily from

David Russinoff 2017-08-01