• 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

• Peripherals

X86-exec-peripherals

Execute the peripherals

Signature

(x86-exec-peripherals x86) → x86

Returns

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

Definitions and Theorems

Function: x86-exec-peripherals

(defun x86-exec-peripherals (x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard t))
 (let ((__function__ 'x86-exec-peripherals))
  (declare (ignorable __function__))
  (b*
   (((when (app-view x86)) x86)
    (time-stamp-counter (n64 (1+ (time-stamp-counter x86))))
    (x86 (!time-stamp-counter time-stamp-counter x86))
    (x86 (if (app-view x86)
             x86
           (wm-low-64 256 time-stamp-counter x86)))
    (last-clock-event (last-clock-event x86))
    (x86 (if (and (> last-clock-event 100000)
                  (equal (rflagsbits->intf (rflags x86))
                         1)
                  (not (inhibit-interrupts-one-instruction x86))
                  (not (equal (memi 264 x86) 0))
                  (not (fault x86)))
             (b* ((x86 (!last-clock-event 0 x86))
                  (x86 (!fault (cons '(:interrupt 32) (fault x86))
                               x86)))
               x86)
           (!last-clock-event (1+ last-clock-event)
                              x86)))
    (x86 (b* ((tty-byte-valid (not (equal (memi 1017 x86) 0)))
              ((when (not tty-byte-valid)) x86)
              (tty-output-byte (memi 1016 x86))
              (x86 (!memi 1017 0 x86))
              (x86 (write-tty tty-output-byte x86)))
           x86))
    (x86 (b* ((tty-write-byte-valid (not (equal (memi 1019 x86) 0)))
              ((when tty-write-byte-valid) x86)
              ((mv tty-input x86) (read-tty x86))
              ((when (equal tty-input nil)) x86)
              (x86 (!memi 1018 tty-input x86))
              (x86 (!memi 1019 1 x86)))
           x86)))
   x86)))

Theorem: x86p-of-x86-exec-peripherals

(defthm x86p-of-x86-exec-peripherals
  (implies (x86p x86)
           (b* ((x86 (x86-exec-peripherals x86)))
             (x86p x86)))
  :rule-classes :rewrite)