# 6.6  Denormal Rounding

The rounding of numbers that lie below the normal range of a floating-point format is conveniently defined by the following function. Note that its arguments include the format itself, both parameters of which are required to compute the precision of the result.

Definition 6.6.1   (drnd) Let be a format and let , .

It is not true in general that , since a non-zero denormal may be rounded to 0. However, we do have the following analog of Lemma 6.5.5.

(drnd-minus) Let be a format and let , . Let be a common rounding mode and let

Then

PROOF: This follows from Lemmas 6.5.5 and 4.1.13

A denormal is always rounded to a representable number, which may be denormal, 0, or the smallest representable normal.

(drnd-exactp-a) Let be a format and let , . Let be a common rounding mode. Then one of the following is true:

(a) .

(b) .

(c) is representable as a denormal in .

PROOF: We may assume , as the general result follows easily from this case.

Let . Suppose first that . Then by Lemmas 6.5.3, 6.1.1, and 6.2.4, either

or

We may assume, therefore, that , so that

and hence,

Since , , i.e.,

By Lemma 6.5.6, is -exact. If , then we have is representable as a denormal. If not, then Lemma 6.5.10 implies . In this case, either and

or and

which implies that is representable as a denormal.

(drnd-exactp-b) If is representable as a denormal in and is a common rounding mode, then

PROOF: Let . By Definition 5.3.5, is -exact. Therefore, by Lemma 6.5.7,

(drnd-exactp-c) If is a format, is a common rounding mode, and with

then iff is -exact.

PROOF: Suppose . Since , Lemma 6.6.2 guarantees that is representable as a denormal, which implies that is -exact.

On the other hand, if is -exact, then is representable by Definition 5.3.5 and by Lemma 6.6.3

(drnd-exactp-d, drnd-exactp-e) Let be a format and let , . Let be representable as a denormal in and let be a common rounding mode.

(a) If , then .

(b) If , then .

PROOF: By Definition 5.3.5, is -exact. The result follows from Lemma 6.5.8

The defining characteristics of the directed rounding modes are inherited by denormal rounding.

(drnd-rtz, drnd-raz, drnd-rup, drnd-rdn)
Let be a format and let , .

(a) .

(b) .

(c) .

(d) .

PROOF: This is a consequence of Lemmas 6.1.5, 6.2.5, 6.5.2, and 6.5.1

Denormal rounding error is bounded by the distance between successive representable numbers (see Lemma 5.3.5).

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

PROOF: Let . By Lemma 6.5.9,

Naturally, unbiased denormal rounding returns the representable number that is closest to its argument.

(drnd-rne-diff,drnd-rna-diff) Let be a format and let , . Let be representable as a denormal in . Then

and

PROOF: By Definition 5.3.5, is -exact. The result follows from Lemmas 6.3.14 and 6.3.35

(drnd-rto) Let be a format and let , . Let be a common rounding mode. If

then

PROOF: See Lemma 6.5.17

The next lemma, which pertains to the detection of floating-point underflow, warrants some motivation. Let be the precise numerical result of an arithmetic operation, to be rounded according to a mode and encoded in a format with precision . Most implementations first compute the value , using an internal format with a sufficient wide exponent field to accommodate this result. According to the x86 architectural definition, underflow occurs when . If this occurs and the underflow mask is set, then the value is computed and returned, and the underflow flag is set iff .

There are, however, implementations that compute directly in the event that , without computing . The requirement of correctly setting the underflow flag then presents a problem, since may lie below the normal range when does not. Thus, for such an implementation, if , then extra logic is required to determine whether . On the other hand, there is no such ambiguity requiring extra logic for the case , since the following lemma guarantees that as well.

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

PROOF: Let . By Lemma 6.5.10, , and hence

Since , the claim follows from Lemma 6.5.18 with and

The next lemma pertains to the setting of the precision flag in the event of underflow and is relevant to the formal architectural specifications discussed in Part III: if is exact, then so is :

Lemma 6.6.11   (rnd-drnd-exactp) Let be a format and let , . Let be a common rounding mode. If , then .

PROOF Let . By lemma6.6.2, is representable as a denormal in , which implies the is -exactp. Since , , and by Lemma 4.2.5, is -exact, and the claim follows from Lemma 6.5.7

We have the following alternative formulation of drnd.

(drnd-rewrite) Let be a format and let , . Let be a common rounding mode. Then

PROOF: Let . We first consider the case and apply Lemma 6.5.13, substituting for , for , and for . Thus,

and is -exact by Lemma 4.2.6. Since

and therefore

as well. Thus, we have

and

The result may be extended to by invoking Lemmas 6.5.5 and 6.6.1: if is defined as in these lemmas, then

Lemma 6.6.12 is used in the proof of the final lemma of this chapter, which pertains to the rounding of numbers smaller than the smallest representable denormal.

(drnd-tiny-a, drnd-tiny-b, drnd-tiny-c)
Let be a format, , and a common rounding mode.

(a) If , then

(b) If , then

(c) If , then

PROOF: Let , , and

By Lemma 6.6.12,

Case 1: or

By Lemma 6.2.5,

and hence, by Lemmas 6.2.11 and 4.2.16,

On the other hand, since

Lemma 6.2.14 implies , and therefore , and

Case 2: or

First note that by Lemma 4.2.20,

Now by Lemma 6.1.5,

and hence, by Lemmas 6.1.9 and 4.2.21,

On the other hand, Lemma 6.1.11 implies , and therefore and

Case 3: or

By Lemmas 6.3.1 and 6.3.22, is either or , and hence is either 0 or , respectively.

Since

and

the claims (a) and (c) follow from Lemmas 6.3.10 and 6.3.31. For the proof of (c), suppose . Then

and . Thus, is -exact but not -exact. The case now follows from Lemma 6.3.21, and since is not -exact, the case follows from Lemma 6.3.39

As a consequence of Lemma 6.6.13 (a), for any given rounding mode, two sufficiently small numbers produce the same rounded result.

Corollary 6.6.14   (drnd-tiny-equal) Let , . Let be a format and a common rounding mode. If

and

then

David Russinoff 2017-08-01