• 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
        • Model-validation
        • Modelcalls
          • X86-out
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • X86isa

Modelcalls

Modelcalls, like syscalls, but instead of calling into the OS, we call into the model.

A modelcall is like a syscall, but it calls into the model asking it to do something. Model calls are done by calling the x86-out instruction. On a real processor this would write to the IO bus, but our processor doesn't support that.

At the moment, one model call is supported. Writing any byte to port 1 results in printing out the null terminated string of one byte characters pointed to by rbx.

Subtopics

X86-out