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: