• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-linux
      • Introduction
      • Asmtest
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
        • Structures
          • Rflagsbits
          • Cr4bits
          • Xcr0bits
          • Cr0bits
          • Prefixes
          • Ia32_eferbits
          • Evex-byte1
          • Cr3bits
          • Evex-byte3
          • Vex3-byte2
          • Vex3-byte1
          • Vex2-byte1
          • Evex-prefixes
          • Evex-byte2
          • Vex-prefixes
          • Sib
          • Modr/m-structures
          • Vex-prefixes-layout-structures
          • Sib-structures
          • Legacy-prefixes-layout-structure
          • Evex-prefixes-layout-structures
          • Cr8bits
          • Opcode-maps-structures
          • Segmentation-bitstructs
          • 8bits
          • 2bits
          • 4bits
          • 16bits
          • Paging-bitstructs
          • 3bits
          • 11bits
          • 40bits
          • 5bits
          • 32bits
          • 19bits
          • 10bits
          • 7bits
          • 64bits
          • 54bits
          • 45bits
          • 36bits
          • 31bits
          • 24bits
          • 22bits
          • 17bits
          • 13bits
          • 12bits
          • 6bits
          • Vex->x
          • Vex->b
          • Vex-prefixes-map-p
          • Vex-prefixes-byte0-p
          • Vex->w
          • Vex->vvvv
          • Vex->r
          • Fp-bitstructs
            • Mxcsrbits
            • Fp-statusbits
            • Mxcsrbits-debug
            • Mxcsrbits-equiv-under-mask
            • Fp-statusbits-equiv-under-mask
            • Fp-statusbits-debug
          • Cr4bits-debug
          • Vex->pp
          • Vex->l
          • Rflagsbits-debug
          • Evex->v-prime
          • Evex->z
          • Evex->w
          • Evex->vvvv
          • Evex->vl/rc
          • Evex->pp
          • Evex->aaa
          • Xcr0bits-debug
          • Vex3-byte1-equiv-under-mask
          • Vex3-byte2-equiv-under-mask
          • Vex2-byte1-equiv-under-mask
          • Vex-prefixes-equiv-under-mask
          • Rflagsbits-equiv-under-mask
          • Ia32_eferbits-equiv-under-mask
          • Evex-prefixes-equiv-under-mask
          • Evex-byte3-equiv-under-mask
          • Evex-byte2-equiv-under-mask
          • Evex-byte1-equiv-under-mask
          • Cr0bits-debug
          • Xcr0bits-equiv-under-mask
          • Sib-equiv-under-mask
          • Prefixes-equiv-under-mask
          • Cr8bits-equiv-under-mask
          • Cr4bits-equiv-under-mask
          • Cr3bits-equiv-under-mask
          • Cr0bits-equiv-under-mask
          • Vex3-byte1-debug
          • Prefixes-debug
          • Ia32_eferbits-debug
          • Evex-byte1-debug
          • Vex3-byte2-debug
          • Vex2-byte1-debug
          • Vex-prefixes-debug
          • Evex-prefixes-debug
          • Evex-byte3-debug
          • Evex-byte2-debug
          • Cr3bits-debug
          • Sib-debug
          • Cr8bits-debug
        • Utilities
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Structures

Fp-bitstructs

Bitstructs related to floating-point operations

Subtopics

Mxcsrbits

The MXCSR Control and Status Register.

Fp-statusbits

The x87 FPU Status Register.

Mxcsrbits-debug

Mxcsrbits-equiv-under-mask

Fp-statusbits-equiv-under-mask

Fp-statusbits-debug