• 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
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
          • Tty
          • Timer
          • X86-exec-peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • X86isa

Peripherals

The various peripherals the x86isa model contains

The x86isa model supports a couple of peripherals. They only work when the enable-peripherals field of the x86 stobj is t. These include a timer and TTY. See their respective documentation topics below.

The primary limitation when writing peripherals for the model is that the state can't change when memory is read. This is signficant because many real life peripherals change state when values are read from their memory mapped interface.

Subtopics

Tty
A TTY device for the x86isa.
Timer
The timer device
X86-exec-peripherals
Execute the peripherals