8  SSE Floating-Point Instructions

The SSE floating-point instructions perform operations on single-precision or double-precision data (Definition 5.1.3) residing in the 128-bit XMM registers or the 256-bit YMM registers. Some SSE instructions are packed, i.e., they partition their operands into several floating-point numbers to be processed in parallel; others are scalar, i.e., they perform a single operation, usually on data comprising the low-order bits of their register arguments.

A single dedicated 16-bit register, the MXCSR, controls and records the response to exceptional conditions that arise during the execution of SSE floating-point operations and controls the rounding of floating-point values.

The behavioral specifications of the scalar instructions presented in this section are formalized by a set of ACL2 functions corresponding to the operations of interest:

Each of these functions takes one or more operands (single- or double-precision floating-point encodings), the initial contents of the MXCSR register, and the data format $ f$ of the instruction, either SP or DP. The function sse-binary-spec, which applies to the four binary arithmmetic operations, takes an additional argument, op, representing the operation (add, sub, mul, or div).

Each function returns two values: the data result and the final value of the MXCSR. For some operands, the specification does not define a value, in which case NIL is returned as the data value. Thus, the correctness of an ACL2 model of an implementation may be verified by proving a theorem stating that for any inputs, the model returns the same MXCSR value as the specification, and in the event that the specification returns a non-NIL data value, the model returns that as well. (N.B.: The specifications of the packed instructions have not yet been formalized.)

David Russinoff 2017-08-01