• 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
            • Read-tty
            • Write-tty
            • Tty-bufferp
          • Timer
          • X86-exec-peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Peripherals

Tty

A TTY device for the x86isa.

In our effort to boot Linux on the x86isa model, it was desirable to have a TTY device to allow us to interact with Linux running on the machine, like one would interact at a shell with any Linux machine. Instead of emulating an existing TTY device, we implement a custom TTY device and implement a Linux driver for it so we could use it under Linux. This device, like all other peripherals, is only available when the enable-peripherals field of the x86 stobj is set to t.

Semantics

Logically this TTY device reads bytes from the list tty-in field on the x86 stobj and writes bytes to the list in the tty-out field. The output in tty-out ends up being in reversed order because new bytes are consed onto the front rather than appended to the end.

By default, this is also how the TTY device behaves in execution. Since such an implementation is difficult to interact with, we provide an additional tty-raw.lsp Common Lisp file which may be included with include-raw (which requires an active trust tag) that opens a TCP socket (on localhost port 6444) and smashes the definitions of read-tty and write-tty so that the TTY reads and writes to the opened TCP socket. This allows interaction with the model by connecting to the TCP socket with programs like netcat or socat. tty-raw.lisp depends on CCL specific code to open the socket, so it only works on ACL2 running under CCL.

Interface

The TTY device presents a simple memory mapped interface to software. If a byte is available for reading the byte at memory address #x3FB is set to 1. The byte may be read from memory address #x3FA. Once the byte has been read, the software should set #x3FB to 0 to allow TTY to write a new byte. If another byte is present in the buffer, it will be available in memory before the next instruction is executed.

Writing to the TTY is similar. To write a byte, write the byte to #x3F8 and then write a non-zero value to #x3F9. Before the next instruction is executed, the TTY device will set #x3F9 to zero.

Subtopics

Read-tty
Read a byte from the TTY.
Write-tty
Write a byte to the TTY.
Tty-bufferp
Recognizer for the TTY buffers.