10  ARM AArch32 Floating-Point Instructions

The elementary arithmetic floating-point instructions of the ARM architecture are similar to the corresponding SSE intructuctions, including both single-operation and vector (SIMD) versions. The architecture provides a floating-point status and control register, (FPSCR), similar to the MXCSR. A significant difference between SSE and ARM, however, is that the FPSCR does not include exception masks--all instructions are effectively masked. Consequently, an ARM instruction always executes to completion and returns a data result, and there is no interaction between the component operations of a SIMD instruction of the sort described in Section 8.2. However, the FPSCR does contain trap enable bits corresponding to the flags. If the trap enable bit is set when an exceptional condition occurs, then upon of completion of the instruction, hardware passes control to a trap handler instead of setting the flag.

Since the operations of a SIMD instruction behave independently, we shall confine our attention to the behavior of scalar instructions. The specifications of the instructions presented in this section are again formalized by a set of three ACL2 functions:

Unlike the corresponding SSE functions, each of these always returns a data result as well as an updated FPSCR. Furthermore, in addition to SP, and DP, the 16-bit format HP is allowed as a value of the parameter $ f$.

David Russinoff 2017-08-01