# 8.4  SSE Post-Computation Exceptions

The procedure described in this section is formalized by the functions sse-binary-post-comp, sse-sqrt-post-comp, and sse-fma-post-comp. Each of these functions calls sse-round, which performs the rounding and detects exceptions.

Unless terminated in response to a pre-computation exceptional condition, each operation of an SSE arithmetic instruction computes an unrounded value, which is then processed according to the contents of the MCXSR and the floating-point format of the instruction as described below. This may result in the setting of one or more exception flags. In the case of a packed instruction, all operations for which a default QNaN value has not been determined in the pre-computation stage are similarly processed in parallel. If any operation produces an unmasked exception, no result is written for any operation. Otherwise, a final result is written for each operation. For an operation that was not terminated in the pre-computation stage, the derivation of this result and the setting of exception flags are determined according to the following case analysis.

If the computed value is infinite or 0, then no flags are set and the sign of the result is determined by the signs of the operands and the rounding mode    MXCSR:

• Infinity: The result is an infinity with sign determined according to the operation:

• Addition: The sign of the infinite operand or operands.

• Subtraction: The sign of the minuend if it is infinite, and otherwise the inverse of the sign of the subtrahend.

• Multiplication or division: The product (xor) of the signs of the operands.

• Square root: The sign of the operand, which must be positive.

• Multiply-accumulate: The sign of the addend if it is infinite, and otherwise the product (xor) of the signs of the factors.

• Zero: The result is a zero with sign determined according to the operation:

• Addition: The sign of operands if they agree; if not, then negative if , and otherwise positive.

• Subtraction: The sign of the minuend if it is the inverse of that of the subtrahend; if not, then negative if , and otherwise positive.

• Multiplication or division: The product (xor) of the signs of the operands.

• Square root: The sign of the operand.

• Multiply-accumulate: The product of the signs of the factors if it agrees with that of the addend; if not, then negative if , and otherwise positive.

Otherwise, the precise mathematical result of the operation (which, of course, need not be computed explicitly by an implementation) is a finite non-zero value . Unless is a denormal, it is rounded according to the rounding mode and the precision of the data format , producing a value . This value is subjected to the following case analysis:

• Overflow ( is above the normal range of the target format, i.e., ): In all cases, OE is set.

• Masked Overflow (OM = 1):

PE is set. The final result, which is valid only if PM = 1, depends on and the sign of .

If (a) , (b) and , or (c)  and , then the final result is an infinity with the sign of .

Otherwise, the result is the encoding of the maximum normal value for the target format, , with the sign of .

• Unmasked Overflow (OM = 0):

No final result is returned. If , then PE is set.

• Underflow ( is below the normal range, i.e., ):
• Masked Underflow (UM = 1):

If FTZ = 1, then UE and PE are set. The final result, which is valid only if PM = 1, is a zero with the sign of .

If FTZ = 0, then is rounded to produce , which may be a denormal value, 0, or the smallest normal, . If , then both UE and PE are set; otherwise, neither flag is modified. The final result, which is valid unless PE is set and PM = 1, is the encoding of , with the sign of if .

• Unmasked Underflow (UM = 0):

UE is set. No final result is returned. If the , then PE is set.

• Normal Case ( is within the normal range, i.e., ):

If , then PE is set. The final result, which is valid unless PE is set and PM = 1, is the normal encoding of .

Thus, PE indicates either that the rounded result is an inexact approximation of an intermediate result, or that some other value has been written to the destination. In the case of masked underflow, it may not be obvious that the behavior described above is consistent with the definition of the auxiliary ACL2 function LREF sse-round, which sets PE if either or . However, Lemma 6.6.11 guarantees that if the first inequality holds, then so does the second.

Also note there is one case in which underflow occurs and UE is not modified: UM = 1 and the unrounded value is returned as a denormal.

David Russinoff 2017-08-01