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

• Tty

Write-tty

Write a byte to the TTY.

Signature

(write-tty c x86) → x86

Returns

x86 — Type (x86p x86), given (x86p x86).

This function writes a byte to the tty-out field of the x86 state by consing the byte to the front of it. Including tty-raw.lsp in raw lisp smashes this function to write to a TCP port instead.

Definitions and Theorems

Function: write-tty

(defun write-tty (c x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (unsigned-byte 8) c))
  (let ((__function__ 'write-tty))
    (declare (ignorable __function__))
    (!tty-out (cons c (tty-out x86)) x86)))

Theorem: x86p-of-write-tty

(defthm x86p-of-write-tty
  (implies (x86p x86)
           (b* ((x86 (write-tty c x86)))
             (x86p x86)))
  :rule-classes :rewrite)