• 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.1.2 Binary Arithmetic Instructions
          • 5.1.1 Data Transfer Instructions
          • 5.1.16 BMI1 and BMI2 Instructions
          • 5.1.5 Shift and Rotate Instructions
          • 5.1.4 Logical Instructions
          • 5.1.7 Control Transfer Instructions
          • 5.1.6 Bit and Byte Instructions
          • 5.1.13 Miscellaneous Instructions
          • 5.1.15 Random Number Generator Instructions
          • 5.1.8 String Instructions
          • 5.1.9 I/O Instructions
          • 5.1.14 User Mode Extended State Save/Restore Instructions
          • 5.1.11 Flag Control (EFLAG) Instructions
          • 5.1.10 Enter and Leave Instructions
          • 5.1.3 Decimal Arithmetic Instructions
          • 5.1.12 Segment Register 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
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• 5.1 General-Purpose Instructions

5.1.15 Random Number Generator Instructions

This group consists of only RDRAND and RDSEED. RDRAND is implemented -- logically, it returns an undefined value (see undef-read), and in execution it produces a random number using Common Lisp's random. RDSEED is not implemented. From the manual it seems like it could be logically described similarly to RDRAND, but should produce "better" random numbers.

Unimplemented Instructions

Opcode	Mnemonic	Other Information	Semantic Function
NP 0F C7	RDSEED	:PFX :NO-PREFIX :REG 7 :FEAT :RDSEED

Implemented Instructions

Opcode	Mnemonic	Other Information	Semantic Function
NP 0F C7	RDRAND	:PFX :NO-PREFIX :REG 6 :MOD 3 :FEAT :RDRAND	x86-rdrand
66 0F C7	RDRAND	:PFX :66 :REG 6 :MOD 3 :FEAT :RDRAND	x86-rdrand