• 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
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
            • Two-byte-opcodes
            • One-byte-opcodes
            • Fp-opcodes
            • Instruction-semantic-functions
              • Sar-spec
              • Shr-spec
              • Sal/shl-spec
              • Rol-spec
              • Ror-spec
              • Rcl-spec
              • Rcr-spec
              • Simd-sub-spec
              • Simd-add-spec
              • Imul-spec
              • Mul-spec
              • Idiv-spec
              • Div-spec
              • Shrd-spec
              • Shld-spec
              • Gpr-arith/logic-spec
              • Shrx-spec
              • Shlx-spec
              • Sarx-spec
              • Floating-point-specifications
                • Floating-point-converts
                  • Sse-cvt-fp1-to-fp2-special
                  • Sse-cvt-fp-to-int
                  • Sse-cvt-int-to-fp
                  • Sp-sse-cvt-int-to-fp
                  • Dp-sse-cvt-int-to-fp
                  • Sp-sse-cvt-fp-to-int
                  • Dp-sse-cvt-fp-to-int
                  • Sse-cvt-sp-to-dp
                  • Sse-cvt-fp-to-int-special
                  • Sse-cvt-dp-to-sp
                  • Rat-round-to-int
                  • Denormalp
                  • Rat-round-to-int-ru
                  • Rat-round-to-int-rd
                  • Rat-round-to-int-rz
                  • Rat-round-to-int-rn
                • Floating-point-arithmetic-specifications
                • Basic-floating-point-utilities
                • Floating-point-comparison-specifications
            • X86-illegal-instruction
            • Implemented-opcodes
            • Opcode-maps
            • X86-general-protection
            • X86-device-not-available
            • X86-step-unimplemented
            • Privileged-opcodes
            • Three-byte-opcodes
          • Register-readers-and-writers
          • X86-modes
          • Segmentation
          • Other-non-deterministic-computations
          • Environment
          • Paging
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Floating-point-specifications

Floating-point-converts

Specification of floating-point conversion operations

Subtopics

Sse-cvt-fp1-to-fp2-special
Check whether the operand is SNaN or QNaN and then return corresponding result. Also handle the infinities.
Sse-cvt-fp-to-int
Sse-cvt-int-to-fp
Sp-sse-cvt-int-to-fp
Dp-sse-cvt-int-to-fp
Sp-sse-cvt-fp-to-int
Dp-sse-cvt-fp-to-int
Sse-cvt-sp-to-dp
Sse-cvt-fp-to-int-special
Check whether the operand is NaN or infinity. If so, return the integer indefinite.
Sse-cvt-dp-to-sp
Rat-round-to-int
Denormalp
Rat-round-to-int-ru
Rat-round-to-int-rd
Rat-round-to-int-rz
Rat-round-to-int-rn