9  x87 Instructions

Our analysis of x87 instructions benefits from two simplifications relative to the SSE architecture: all instructions are scalar and there is no multiply-accumulate instruction. Thus, every instruction to be considered here consists of a single operation on one or two operands.

The x87 architecture provides an array of eight 80-bit data registers, which is managed as a circular stack. Each numerical operand is located either in an x87 data register or in memory and is interpreted according to one of the data formats defined by Definition 5.1.3. Data register contents are always interpreted according to the double extended precision format (EP). Memory operands may be encoded in the single (SP), double (DP), or double extended precision format. Numerical results are written only to the data registers in the EP format.

The architecture also provides distinct 16-bit control and status registers, the FCW and the FSW, corresponding to the single SSE register MXCSR.

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

Each of these functions takes one or two operands and the corresponding formats, each of which may be SP, DP, or EP, and the initial contents of the FCW and FSW registers. The function x87-binary-spec, which applies to the binary arithmetic operations, takes an additional argument representing the operation (add, sub, mul, or div).

Each function returns two values: the data result and the final value of the FSW. 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 FSW value as the specification, and in the event that the specification returns a non-NIL data value, the model returns that as well.

David Russinoff 2017-08-01