• 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-lazy

Signature

(svtv-compile-lazy nphases 
                   ins overrides outs prev-state updates 
                   state-updates in-vars state-machine) 
 
  → 
(mv outalist final-state)

Arguments

nphases — Guard (posp 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).

Definitions and Theorems

Function: svtv-compile-lazy

(defun svtv-compile-lazy
       (nphases ins overrides outs prev-state updates
                state-updates in-vars state-machine)
 (declare (xargs :guard (and (posp 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))))
 (let ((__function__ 'svtv-compile-lazy))
  (declare (ignorable __function__))
  (b*
   (((with-fast prev-state updates state-updates))
    (in-alists
         (svtv-allphases-inputs 0 nphases ins overrides in-vars))
    (state-vars
         (acl2::hons-remove-dups (svex-alist-keys state-updates)))
    (state-updates
         (with-fast-alist
              state-updates
              (svex-alist-extract state-vars state-updates)))
    (prev-state
       (with-fast-alist prev-state
                        (svex-alist-extract state-vars prev-state)))
    (composedata
         (svtv-precompose-phases
              (lposfix nphases)
              (make-svtv-precompose-data
                   :nextstate state-updates
                   :input-substs (make-fast-alists in-alists)
                   :initst prev-state)))
    ((mv outalist final-state)
     (svtv-compile-phases-lazy 0 nphases outs
                               updates composedata state-machine)))
   (fast-alist-free-list in-alists)
   (clear-memoize-table 'svex-compose)
   (clear-memoize-table 'svex-compose-svtv-phases-call)
   (mv outalist final-state))))

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

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

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

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

Theorem: svtv-compile-lazy-of-pos-fix-nphases

(defthm svtv-compile-lazy-of-pos-fix-nphases
  (equal (svtv-compile-lazy (pos-fix nphases)
                            ins overrides outs prev-state updates
                            state-updates in-vars state-machine)
         (svtv-compile-lazy nphases
                            ins overrides outs prev-state updates
                            state-updates in-vars state-machine)))

Theorem: svtv-compile-lazy-pos-equiv-congruence-on-nphases

(defthm svtv-compile-lazy-pos-equiv-congruence-on-nphases
 (implies
    (pos-equiv nphases nphases-equiv)
    (equal (svtv-compile-lazy nphases
                              ins overrides outs prev-state updates
                              state-updates in-vars state-machine)
           (svtv-compile-lazy nphases-equiv
                              ins overrides outs prev-state updates
                              state-updates in-vars state-machine)))
 :rule-classes :congruence)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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