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:
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:
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 .
No final result is returned. If , then PE is set.
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 .
UE is set. No final result is returned. If the , then PE is set.
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