• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
        • 5.50 Uncategorized "Instructions"
        • 5.15 Fused-Multiply-Add (FMA)
        • 5.20 System Instructions
        • 5.19 Intel(R) Advanced Vector Extensions 512 (Intel(R) AVX-512)
        • 5.1 General-Purpose Instructions
        • 5.10 Intel(R) SSE4.1 Instructions
        • 5.13 Intel(R) Advanced Vector Extensions (Intel(R) AVX)
        • 5.7 Intel(R) SSE3 Instructions
        • 5.8 Supplemental Streaming Simd Extensions 3 (SSSE3) Instructions
        • 5.4 MMX Instructions
        • 5.22 Virtual-Machine Extensions
        • 5.6 Intel(R) SSE2 Instructions
        • 5.21 64-Bit Mode Instructions
        • 5.2 X87 FPU Instructions
          • 5.2.2 X87 FPU Basic Arithmetic Instructions
          • 5.2.1 X87 FPU Data Transfer Instructions
          • 5.2.6 X87 FPU Control Instructions
          • 5.2.3 X87 FPU Comparison Instructions
          • 5.2.4 X87 FPU Transcendental Instructions
          • 5.2.5 X87 FPU Load Constants Instructions
        • 5.24 Intel(R) Memory Protection Extensions
        • 5.5 Intel(R) SSE Instructions
        • 5.16 Intel(R) Advanced Vector Extensions 2 (Intel(R) AVX2)
        • 5.12 Intel(R) AES-NI And PCLMULQDQ
        • 5.17 Intel(R) Transactional Synchronization Extensions (Intel(R) Tsx)
        • 5.14 16-Bit Floating-Point Conversion
        • 5.18 Intel(R) SHA Extensions
        • 5.11 Intel(R) SSE4.2 Instruction Set
        • 5.3 X87 FPU and SIMD State Management Instructions
        • 5.40 Other ISA Extensions
        • 5.25 Intel(R) Software Guard Extensions
        • 5.27 Control Transfer Terminating Instructions
        • 5.23 Safer Mode Extensions
        • 5.30 Enqueue Store Instructions
        • 5.29 User Interrupt Instructions
        • 5.28 Intel(R) AMX Instructions
        • 5.26 Shadow Stack Management Instructions
        • 5.31 Intel(R) Advanced Vector Extensions 10 Version 1 Instructions
      • Tlb
      • Running-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• 5.2 X87 FPU Instructions

5.2.6 X87 FPU Control Instructions

Note a few of X86 control instructions are listed in the SDM as being encoded using 0x9B as a prefix. This is a bit weird since 9B is also an opcode on its own, FWAIT/WAIT. It seems as though the behavior of these 9B-prefixed instructions is basically to wait for exceptions and then (if no exception) do what the instruction. Not sure why they are listed that way.

Unimplemented Instructions

Opcode	Mnemonic	Other Information	Semantic Function
D9	FLDENV	:REG 4 :MOD :MEM :FEAT :FPU
D9	FLDCW	:REG 5 :MOD :MEM :FEAT :FPU
D9	FNSTENV	:REG 6 :MOD :MEM :FEAT :FPU
D9	FNSTCW	:REG 7 :MOD :MEM :FEAT :FPU
D9	FNOP	:REG 2 :MOD 3 :R/M 0 :FEAT :FPU
D9	FDECSTP	:REG 6 :MOD 3 :R/M 6 :FEAT :FPU
D9	FINCSTP	:REG 6 :MOD 3 :R/M 7 :FEAT :FPU
DB	FNCLEX	:REG 4 :MOD 3 :R/M 2 :FEAT :FPU
DB	FNINIT	:REG 4 :MOD 3 :R/M 3 :FEAT :FPU
DD	FRSTOR	:REG 4 :MOD :MEM :FEAT :FPU
DD	FNSAVE	:REG 6 :MOD :MEM :FEAT :FPU
DD	FNSTSW	:REG 7 :MOD :MEM :FEAT :FPU
DD	FFREE	:REG 0 :MOD 3 :FEAT :FPU
DF	FNSTSW	:REG 4 :MOD 3 :R/M 0 :FEAT :FPU

Implemented Instructions

Opcode	Mnemonic	Other Information	Semantic Function
9B	FWAIT/WAIT		x86-one-byte-nop