• 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Process.lisp

Svtv-compile

Signature

(svtv-compile phase nphases ins overrides outs 
              prev-state updates state-updates in-vars 
              keep-final-state keep-all-states) 
 
  → 
(mv outalist final-state all-states)

Arguments

phase — Guard (natp phase).

nphases — Guard (natp nphases).

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).

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

all-states — Type (svex-alistlist-p all-states).

Definitions and Theorems

Function: svtv-compile

(defun svtv-compile (phase nphases ins overrides outs
                           prev-state updates state-updates in-vars
                           keep-final-state keep-all-states)
  (declare (xargs :guard (and (natp phase)
                              (natp nphases)
                              (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))))
  (declare (xargs :guard (<= phase nphases)))
  (let ((__function__ 'svtv-compile))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp (- (nfix nphases) (nfix phase)))
                     :exec (eql nphases phase)))
          (mv nil
              (and keep-final-state
                   (svex-alist-fix prev-state))
              (and keep-all-states
                   (list (svex-alist-fix prev-state)))))
         ((mv phase-outs next-state)
          (svtv-compile-phase phase ins overrides outs prev-state
                              updates state-updates in-vars))
         ((mv rest-outs final-state all-states)
          (svtv-compile (+ 1 (lnfix phase))
                        nphases ins overrides outs
                        next-state updates state-updates in-vars
                        keep-final-state keep-all-states)))
      (mv (append phase-outs rest-outs)
          final-state
          (and keep-all-states
               (cons (svex-alist-fix prev-state)
                     all-states))))))

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

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

Theorem: svex-alist-p-of-svtv-compile.final-state

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

Theorem: svex-alistlist-p-of-svtv-compile.all-states

(defthm svex-alistlist-p-of-svtv-compile.all-states
  (b* (((mv ?outalist ?final-state ?all-states)
        (svtv-compile phase nphases ins overrides outs
                      prev-state updates state-updates in-vars
                      keep-final-state keep-all-states)))
    (svex-alistlist-p all-states))
  :rule-classes :rewrite)

Theorem: svtv-compile-of-nfix-phase

(defthm svtv-compile-of-nfix-phase
  (equal (svtv-compile (nfix phase)
                       nphases ins overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)
         (svtv-compile phase nphases ins overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)))

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

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

Theorem: svtv-compile-of-nfix-nphases

(defthm svtv-compile-of-nfix-nphases
  (equal (svtv-compile phase (nfix nphases)
                       ins overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)
         (svtv-compile phase nphases ins overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)))

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

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

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

(defthm svtv-compile-of-svtv-lines-fix-ins
  (equal (svtv-compile phase nphases (svtv-lines-fix ins)
                       overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)
         (svtv-compile phase nphases ins overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)))

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

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

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

(defthm svtv-compile-of-svtv-overridelines-fix-overrides
  (equal (svtv-compile phase nphases
                       ins (svtv-overridelines-fix overrides)
                       outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)
         (svtv-compile phase nphases ins overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)))

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

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

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

(defthm svtv-compile-of-svtv-lines-fix-outs
  (equal (svtv-compile phase nphases
                       ins overrides (svtv-lines-fix outs)
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)
         (svtv-compile phase nphases ins overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defthm svtv-compile-of-svarlist-fix-in-vars
  (equal (svtv-compile phase nphases
                       ins overrides outs prev-state updates
                       state-updates (svarlist-fix in-vars)
                       keep-final-state keep-all-states)
         (svtv-compile phase nphases ins overrides outs
                       prev-state updates state-updates in-vars
                       keep-final-state keep-all-states)))

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

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