• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • 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
            • Addr-range
            • Read-from-physical-memory
            • Write-to-physical-memory
            • Rm-low-32
            • Wm-low-32
            • Rm-low-64
            • Create-physical-address-list
            • Wm-low-64
            • Physical-address-listp
            • Physical-address-p
          • Decoding-and-spec-utils
          • Instructions
          • 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
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Machine

Physical-memory

Physical memory read and write functions

Note that the top-level memory accessor function is rme08 and updater function is wme08. Their 16, 32, 64, and 128 bit counterparts are also available. These functions behave differently depending upon the value of app-view.

The functions defined here, like rm-low-32 and wm-low-32, are low-level read and write functions that access physical memory directly in the system-level view. We do not recommend using these functions at the top-level.

Subtopics

Addr-range
Read-from-physical-memory
Write-to-physical-memory
Rm-low-32
Wm-low-32
Rm-low-64
Create-physical-address-list
Wm-low-64
Physical-address-listp
Recognizer of a list of physical addresses
Physical-address-p