• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
        • Svtv-data
        • Defsvtv$
        • Svtv-run
        • Defsvtv-phasewise
        • Svtv
        • Svtv-spec
        • Defsvtv
        • Process.lisp
          • Svtv-compile
          • Defsvtv-events
          • Svtv-compile-lazy
          • Svtv-compile-phase
          • Svtv-compile-phases-lazy
          • Svtv-allphases-inputs
          • Svtv-phase-inputs
          • Svtv-inalist-resolve-unassigned
          • Svtv-simplify-outs/states
          • Svtv-collect-inmap
          • Svar-boolmasks-limit-to-bound-vars
          • Svtv-overrides->assigns
          • Svtv-non-override-test-input-vars
          • Svtv-outputs->outalist
          • Svtv-run-squash-dontcares
          • Svtv-inputs->assigns
          • Svtv-phase-var-assigns
          • Defsvtv-fn
          • Svtv-entries->overrideconds
          • Svtv-entries->vars
          • Svtv-easy-bindings-main
          • Svtv-collect-masks
          • Svtv-baseentry-svex
          • Svtv-init-states
          • Lhs->mask
          • Svtv-easy-bindings-svtv-vars
          • Svtv-autoins-aux
          • Svtv-autohyps-aux
          • Svtv-autobinds-aux
          • Svtv-autoins
          • Svtv-autohyps
          • Svtv-autobinds
          • Fast-alist-free-list
          • Defsvtv-default-names
        • Svtv-doc
        • Svtv-chase$
        • Svtv-versus-stv
        • Svtv-debug-fsm
        • Structure.lisp
        • Svtv-debug
        • Def-pipeline-thm
        • Expand.lisp
        • Def-cycle-thm
        • Svtv-utilities
        • Svtv-debug$
        • Defsvtv$-phasewise
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Process.lisp

Svtv-compile-phase

Signature

(svtv-compile-phase phase ins overrides outs prev-state 
                    updates state-updates in-vars) 
 
  → 
(mv outalist next-state)

Arguments

phase — Guard (natp phase).

ins — Guard (svtv-lines-p ins).

overrides — Guard (svtv-overridelines-p overrides).

outs — Guard (svtv-lines-p outs).

prev-state — Guard (svex-alist-p prev-state).

updates — Guard (svex-alist-p updates).

state-updates — Guard (svex-alist-p state-updates).

in-vars — Guard (svarlist-p in-vars).

Returns

outalist — Type (svex-alist-p outalist).

next-state — Type (svex-alist-p next-state).

Definitions and Theorems

Function: svtv-compile-phase

(defun svtv-compile-phase (phase ins overrides outs prev-state
                                 updates state-updates in-vars)
 (declare (xargs :guard (and (natp phase)
                             (svtv-lines-p ins)
                             (svtv-overridelines-p overrides)
                             (svtv-lines-p outs)
                             (svex-alist-p prev-state)
                             (svex-alist-p updates)
                             (svex-alist-p state-updates)
                             (svarlist-p in-vars))))
 (let ((__function__ 'svtv-compile-phase))
  (declare (ignorable __function__))
  (b* ((input-alist
            (append (svtv-phase-inputs phase ins overrides in-vars)
                    prev-state))
       ((with-fast input-alist updates))
       (outalist
            (svex-alist-compose (svtv-outputs->outalist outs phase)
                                updates))
       (composed-outalist (svex-alist-compose outalist input-alist))
       (next-state (svex-alist-compose state-updates input-alist)))
    (clear-memoize-table 'svex-compose)
    (mv composed-outalist next-state))))

Theorem: svex-alist-p-of-svtv-compile-phase.outalist

(defthm svex-alist-p-of-svtv-compile-phase.outalist
  (b* (((mv ?outalist ?next-state)
        (svtv-compile-phase phase ins overrides outs prev-state
                            updates state-updates in-vars)))
    (svex-alist-p outalist))
  :rule-classes :rewrite)

Theorem: svex-alist-p-of-svtv-compile-phase.next-state

(defthm svex-alist-p-of-svtv-compile-phase.next-state
  (b* (((mv ?outalist ?next-state)
        (svtv-compile-phase phase ins overrides outs prev-state
                            updates state-updates in-vars)))
    (svex-alist-p next-state))
  :rule-classes :rewrite)

Theorem: svtv-compile-phase-of-nfix-phase

(defthm svtv-compile-phase-of-nfix-phase
  (equal (svtv-compile-phase (nfix phase)
                             ins overrides outs prev-state
                             updates state-updates in-vars)
         (svtv-compile-phase phase ins overrides outs prev-state
                             updates state-updates in-vars)))

Theorem: svtv-compile-phase-nat-equiv-congruence-on-phase

(defthm svtv-compile-phase-nat-equiv-congruence-on-phase
 (implies
      (nat-equiv phase phase-equiv)
      (equal (svtv-compile-phase phase ins overrides outs prev-state
                                 updates state-updates in-vars)
             (svtv-compile-phase phase-equiv
                                 ins overrides outs prev-state
                                 updates state-updates in-vars)))
 :rule-classes :congruence)

Theorem: svtv-compile-phase-of-svtv-lines-fix-ins

(defthm svtv-compile-phase-of-svtv-lines-fix-ins
  (equal (svtv-compile-phase phase (svtv-lines-fix ins)
                             overrides outs prev-state
                             updates state-updates in-vars)
         (svtv-compile-phase phase ins overrides outs prev-state
                             updates state-updates in-vars)))

Theorem: svtv-compile-phase-svtv-lines-equiv-congruence-on-ins

(defthm svtv-compile-phase-svtv-lines-equiv-congruence-on-ins
 (implies
      (svtv-lines-equiv ins ins-equiv)
      (equal (svtv-compile-phase phase ins overrides outs prev-state
                                 updates state-updates in-vars)
             (svtv-compile-phase phase
                                 ins-equiv overrides outs prev-state
                                 updates state-updates in-vars)))
 :rule-classes :congruence)

Theorem: svtv-compile-phase-of-svtv-overridelines-fix-overrides

(defthm svtv-compile-phase-of-svtv-overridelines-fix-overrides
  (equal (svtv-compile-phase phase
                             ins (svtv-overridelines-fix overrides)
                             outs prev-state
                             updates state-updates in-vars)
         (svtv-compile-phase phase ins overrides outs prev-state
                             updates state-updates in-vars)))

Theorem: svtv-compile-phase-svtv-overridelines-equiv-congruence-on-overrides

(defthm
 svtv-compile-phase-svtv-overridelines-equiv-congruence-on-overrides
 (implies
      (svtv-overridelines-equiv overrides overrides-equiv)
      (equal (svtv-compile-phase phase ins overrides outs prev-state
                                 updates state-updates in-vars)
             (svtv-compile-phase phase
                                 ins overrides-equiv outs prev-state
                                 updates state-updates in-vars)))
 :rule-classes :congruence)

Theorem: svtv-compile-phase-of-svtv-lines-fix-outs

(defthm svtv-compile-phase-of-svtv-lines-fix-outs
  (equal (svtv-compile-phase phase
                             ins overrides (svtv-lines-fix outs)
                             prev-state
                             updates state-updates in-vars)
         (svtv-compile-phase phase ins overrides outs prev-state
                             updates state-updates in-vars)))

Theorem: svtv-compile-phase-svtv-lines-equiv-congruence-on-outs

(defthm svtv-compile-phase-svtv-lines-equiv-congruence-on-outs
 (implies
      (svtv-lines-equiv outs outs-equiv)
      (equal (svtv-compile-phase phase ins overrides outs prev-state
                                 updates state-updates in-vars)
             (svtv-compile-phase phase
                                 ins overrides outs-equiv prev-state
                                 updates state-updates in-vars)))
 :rule-classes :congruence)

Theorem: svtv-compile-phase-of-svex-alist-fix-prev-state

(defthm svtv-compile-phase-of-svex-alist-fix-prev-state
  (equal (svtv-compile-phase phase ins overrides
                             outs (svex-alist-fix prev-state)
                             updates state-updates in-vars)
         (svtv-compile-phase phase ins overrides outs prev-state
                             updates state-updates in-vars)))

Theorem: svtv-compile-phase-svex-alist-equiv-congruence-on-prev-state

(defthm svtv-compile-phase-svex-alist-equiv-congruence-on-prev-state
 (implies
      (svex-alist-equiv prev-state prev-state-equiv)
      (equal (svtv-compile-phase phase ins overrides outs prev-state
                                 updates state-updates in-vars)
             (svtv-compile-phase phase
                                 ins overrides outs prev-state-equiv
                                 updates state-updates in-vars)))
 :rule-classes :congruence)

Theorem: svtv-compile-phase-of-svex-alist-fix-updates

(defthm svtv-compile-phase-of-svex-alist-fix-updates
 (equal (svtv-compile-phase phase ins overrides
                            outs prev-state (svex-alist-fix updates)
                            state-updates in-vars)
        (svtv-compile-phase phase ins overrides outs prev-state
                            updates state-updates in-vars)))

Theorem: svtv-compile-phase-svex-alist-equiv-congruence-on-updates

(defthm svtv-compile-phase-svex-alist-equiv-congruence-on-updates
 (implies
   (svex-alist-equiv updates updates-equiv)
   (equal (svtv-compile-phase phase ins overrides outs prev-state
                              updates state-updates in-vars)
          (svtv-compile-phase phase ins overrides outs prev-state
                              updates-equiv state-updates in-vars)))
 :rule-classes :congruence)

Theorem: svtv-compile-phase-of-svex-alist-fix-state-updates

(defthm svtv-compile-phase-of-svex-alist-fix-state-updates
  (equal (svtv-compile-phase phase ins overrides outs prev-state
                             updates (svex-alist-fix state-updates)
                             in-vars)
         (svtv-compile-phase phase ins overrides outs prev-state
                             updates state-updates in-vars)))

Theorem: svtv-compile-phase-svex-alist-equiv-congruence-on-state-updates

(defthm
    svtv-compile-phase-svex-alist-equiv-congruence-on-state-updates
 (implies
   (svex-alist-equiv state-updates state-updates-equiv)
   (equal (svtv-compile-phase phase ins overrides outs prev-state
                              updates state-updates in-vars)
          (svtv-compile-phase phase ins overrides outs prev-state
                              updates state-updates-equiv in-vars)))
 :rule-classes :congruence)

Theorem: svtv-compile-phase-of-svarlist-fix-in-vars

(defthm svtv-compile-phase-of-svarlist-fix-in-vars
  (equal (svtv-compile-phase phase
                             ins overrides outs prev-state updates
                             state-updates (svarlist-fix in-vars))
         (svtv-compile-phase phase ins overrides outs prev-state
                             updates state-updates in-vars)))

Theorem: svtv-compile-phase-svarlist-equiv-congruence-on-in-vars

(defthm svtv-compile-phase-svarlist-equiv-congruence-on-in-vars
 (implies
   (svarlist-equiv in-vars in-vars-equiv)
   (equal (svtv-compile-phase phase ins overrides outs prev-state
                              updates state-updates in-vars)
          (svtv-compile-phase phase ins overrides outs prev-state
                              updates state-updates in-vars-equiv)))
 :rule-classes :congruence)