• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • 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.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
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Sdm-instruction-set-summary

5.20 System Instructions

• XRSTORS (0x0FC7 /3) XSAVEC (0x0FC7 /4), and XSAVES (0x0FC7 /5) are missing from the opcode maps
• Removed MOV from the list until I can specify only certain forms of it

Unimplemented Instructions

Opcode	Mnemonic	Other Information	Semantic Function
63	ARPL	:MODE :I64
0F 00	SLDT	:REG 0 :MOD :MEM
0F 00	SLDT	:REG 0 :MOD 3
0F 00	STR	:REG 1 :MOD :MEM
0F 00	STR	:REG 1 :MOD 3
0F 00	VERR	:REG 4
0F 00	VERW	:REG 5
0F 01	SIDT	:REG 1 :MOD :MEM
0F 01	CLAC	:REG 1 :MOD 3 :R/M 2 :FEAT :SMAP
0F 01	STAC	:REG 1 :MOD 3 :R/M 3 :FEAT :SMAP
0F 01	XGETBV	:REG 3 :MOD 3 :R/M 0 :FEAT :XSAVE
0F 01	XSETBV	:REG 3 :MOD 3 :R/M 1 :FEAT :XSAVE
0F 01	SMSW	:REG 4 :MOD :MEM
0F 01	SMSW	:REG 4 :MOD 3
0F 01	LMSW	:REG 6
0F 01	RDTSCP	:REG 7 :MOD 3 :R/M 1 :FEAT :RDTSCP
0F 02	LAR
0F 03	LSL
0F 06	CLTS
0F 08	INVD
0F 09	WBINVD
0F 33	RDPMC
0F 34	SYSENTER
0F 35	SYSEXIT
0F AA	RSM
F3 0F AE	RDFSBASE	:MODE :O64 :PFX :F3 :REG 0 :MOD 3 :FEAT :FSGSBASE
F3 0F AE	RDGSBASE	:MODE :O64 :PFX :F3 :REG 1 :MOD 3 :FEAT :FSGSBASE
F3 0F AE	WRFSBASE	:MODE :O64 :PFX :F3 :REG 2 :MOD 3 :FEAT :FSGSBASE
F3 0F AE	WRGSBASE	:MODE :O64 :PFX :F3 :REG 3 :MOD 3 :FEAT :FSGSBASE
NP 0F AE	XSAVE	:PFX :NO-PREFIX :REG 4 :MOD :MEM :FEAT :XSAVE
NP 0F AE	XRSTOR	:PFX :NO-PREFIX :REG 5 :MOD :MEM :FEAT :XSAVE
NP 0F AE	XSAVEOPT	:PFX :NO-PREFIX :REG 6 :MOD :MEM
66 0F 38 82	INVPCID	:PFX :66

Implemented Instructions

Opcode	Mnemonic	Other Information	Semantic Function
F4	HLT		x86-hlt
0F 00	LLDT	:REG 2	x86-lldt
0F 00	LTR	:REG 3	x86-ltr
0F 01	SGDT	:REG 0 :MOD :MEM	x86-sgdt
0F 01	LGDT	:REG 2 :MOD :MEM	x86-lgdt
0F 01	LIDT	:REG 3 :MOD :MEM	x86-lidt
0F 01	INVLPG	:REG 7 :MOD :MEM	x86-invlpg
0F 30	WRMSR		x86-wrmsr
0F 31	RDTSC		x86-rdtsc
0F 32	RDMSR		x86-rdmsr