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 $ {\cal R} =$   MXCSR$ [14:13]$:

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 $ u$. Unless $ u$ is a denormal, it is rounded according to the rounding mode $ {\cal R}$ and the precision $ p$ of the data format $ F$, producing a value $ r = \mathit{rnd}(u, {\cal R}, p)$. This value is subjected to the following case analysis:

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 $ r \neq u$ or $ d \neq u$. 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