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

    Timer

    The timer device

    The timer device can be used to receive an interrupt every 100,000 instruction executions. If the interrupt flag is zero 100,000 instructions after the last timer interrupt, we wait to send the interrupt until after they get reenabled. To enable this, make sure enable-peripherals on the x86 stobj is t and write a non-zero byte to physical memory address 0x108. Additionally, if to be able to handle the interrupt in software running on the model, make sure the handle-exceptions field of the x86 stobj is also t.

    The timer device also writes the number of instructions that have been executed as a 64-bit unsigned integer to 0x100. This is the same value returned by the x86-rdtsc instruction.