• 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
            • X86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex
            • X86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm
            • X86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm
            • X86-addps/subps/mulps/divps/maxps/minps-op/en-rm
            • X86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm
            • X86-cvts?2si/cvtts?2si-op/en-rm
            • X86-comis?/ucomis?-op/en-rm
            • X86-cmpps-op/en-rmi
            • X86-movups/movupd/movdqu-op/en-rm
            • X86-pmovmskb-op/en-rm
            • X86-unpck?ps-op/en-rm
            • X86-cmppd-op/en-rmi
            • X86-sqrtps-op/en-rm
            • X86-vmovups-vex-b
            • X86-unpck?pd-op/en-rm
            • X86-cvtsi2s?-op/en-rm
            • X86-cmpss/cmpsd-op/en-rmi
            • X86-vmovups-vex-a
            • X86-shufps-op/en-rmi
            • X86-cvtpd2ps-op/en-rm
            • X86-sqrtpd-op/en-rm
            • X86-cvts?2s?-op/en-rm
            • X86-vzeroupper
            • X86-movups/movupd/movdqu-op/en-mr
            • X86-cvtps2pd-op/en-rm
            • X86-sqrts?-op/en-rm
            • X86-shufpd-op/en-rmi
            • X86-movss/movsd-op/en-rm
            • X86-movss/movsd-op/en-mr
            • X86-movhps/movhpd-op/en-mr
            • X86-movaps/movapd-op/en-mr
            • X86-movlps/movlpd-op/en-rm
            • X86-movlps/movlpd-op/en-mr
            • X86-movhps/movhpd-op/en-rm
            • X86-movaps/movapd-op/en-rm
            • X86-ldmxcsr/stmxcsr-op/en-m
            • X86-bsf-op/en-rm
            • X86-movhlps-sse
          • Instruction-semantic-functions
          • 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

• Instructions

Fp-opcodes

Instruction semantic functions for Intel's floating-point instructions

Subtopics

X86-vandp?/vandnp?/vorp?/vxorp?/vpand/vpandn/vpor/vpxor-vex

VEX-encoded logical instructions.

X86-adds?/subs?/muls?/divs?/maxs?/mins?-op/en-rm

Add/Sub/Mul/Div/Max/Min scalar single/double precision floating-point values

X86-andp?/andnp?/orp?/xorp?/pand/pandn/por/pxor-op/en-rm

X86-addps/subps/mulps/divps/maxps/minps-op/en-rm

Add/Sub/Mul/Div/Max/Min packed single-precision floating-point values

X86-addpd/subpd/mulpd/divpd/maxpd/minpd-op/en-rm

Add/Sub/Mul/Div/Max/Min packed double-precision floating-point values

X86-cvts?2si/cvtts?2si-op/en-rm

Convert scalar single/double precision FP value to integer

X86-comis?/ucomis?-op/en-rm

Order/Unordered compare scalar single/double precision floating-point values and set EFLAGS

X86-cmpps-op/en-rmi

Compare packed single-precision floating-point values

X86-movups/movupd/movdqu-op/en-rm

X86-pmovmskb-op/en-rm

Move byte mask

X86-unpck?ps-op/en-rm

Unpack and interleave low/high packed single-precision floating-point values

X86-cmppd-op/en-rmi

Compare packed double-precision floating-point values

X86-sqrtps-op/en-rm

Square roots of packed single-precision floating-point values

X86-vmovups-vex-b

VMOVUPS: Move Unaligned Packed Single Precision Floating-Point Values (VEX encoding, Op/En B)

X86-unpck?pd-op/en-rm

Unpack and interleave low/high packed double-precision floating-point values

X86-cvtsi2s?-op/en-rm

Convert integer to scalar single/double precision FP value

X86-cmpss/cmpsd-op/en-rmi

Compare scalar single/double precision floating-point values

X86-vmovups-vex-a

VMOVUPS: Move Unaligned Packed Single Precision Floating-Point Values (VEX encoding, Op/En A)

X86-shufps-op/en-rmi

Shuffle packed single-precision floating-point values

X86-cvtpd2ps-op/en-rm

Convert packed double-precision FP values to packed single-precision FP values

X86-sqrtpd-op/en-rm

Square roots packed double-precision floating-point values

X86-cvts?2s?-op/en-rm

Convert scalar single/double precision FP value to scalar double/single FP value

X86-vzeroupper

VZEROUPPER: Zero Upper Bits of YMM and ZMM Registers

X86-movups/movupd/movdqu-op/en-mr

X86-cvtps2pd-op/en-rm

Convert packed single-precision FP values to packed double-precision FP values

X86-sqrts?-op/en-rm

Square root of scalar single/double precision floating-point value

X86-shufpd-op/en-rmi

Shuffle packed double-precision floating-point values

X86-movss/movsd-op/en-rm

Move scalar single/double precision floating-point values

X86-movss/movsd-op/en-mr

Move scalar single/double precision floating-point values

X86-movhps/movhpd-op/en-mr

Move high packed single/double precision floating-point values

X86-movaps/movapd-op/en-mr

Move aligned packed single/double precision floating-point values

X86-movlps/movlpd-op/en-rm

Move low packed single/double precision floating-point values

X86-movlps/movlpd-op/en-mr

Move low packed single/double precision floating-point values

X86-movhps/movhpd-op/en-rm

Move high packed single/double precision floating-point values

X86-movaps/movapd-op/en-rm

Move aligned packed single/double precision floating-point values

X86-ldmxcsr/stmxcsr-op/en-m

Load/Store MXCSR register

X86-bsf-op/en-rm

Bit scan forward

X86-movhlps-sse

Move Packed Single Precision Floating-Point Values High to Low