|
|
|---|
|
|
|
|---|
Main subroutine of defsvtv, which extracts output formulas from the provided design.
(defsvtv-main name ins
overrides outs internals design labels
simplify pre-simplify initial-state-vars
keep-final-state keep-all-states form)
→
resFunction:
(defun defsvtv-main (name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (declare (xargs :guard (and (symbolp name) (true-list-listp ins) (true-list-listp overrides) (true-list-listp outs) (true-list-listp internals) (design-p design) (symbol-listp labels)))) (declare (xargs :guard (modalist-addr-p (design->modalist design)))) (let ((__function__ 'defsvtv-main)) (declare (ignorable __function__)) (b* (((acl2::local-stobjs moddb aliases) (mv svtv moddb aliases)) ((mv err assigns delays ?constraints moddb aliases) (svex-design-flatten-and-normalize design)) ((when err) (raise "Error flattening design: ~@0" err) (mv nil moddb aliases)) (modidx (moddb-modname-get-index (design->top design) moddb)) (orig-ins ins) (orig-overrides overrides) (orig-outs outs) (orig-internals internals) ((mv errs1 ins) (svtv-wires->lhses ins modidx moddb aliases)) (input-err (and errs1 (msg "Errors resolving inputs:~%~@0~%" (msg-list errs1)))) ((mv errs2 overrides) (svtv-wires->lhses overrides modidx moddb aliases)) (override-err (and errs2 (msg "Errors resolving overrides:~%~@0~%" (msg-list errs2)))) ((mv errs3 outs) (svtv-wires->lhses (append outs internals) modidx moddb aliases)) (output-err (and errs3 (msg "Errors resolving outputs:~%~@0~%" (msg-list errs3)))) ((when (or input-err override-err output-err)) (raise "~%~@0" (msg-list (list input-err output-err override-err))) (mv nil moddb aliases)) (nphases (pos-fix (max (svtv-max-length ins) (max (svtv-max-length overrides) (svtv-max-length outs))))) (ins (svtv-expand-lines ins nphases)) (overrides (svtv-expand-lines overrides nphases)) ((mv ovlines ovs) (svtv-lines->overrides overrides 0)) (assigns (make-fast-alist assigns)) (overridden-assigns (svex-apply-overrides ovs assigns)) (orig-assigns (make-fast-alist assigns)) (- (fast-alist-free overridden-assigns)) ((mv updates next-states ?constraints) (svex-compose-assigns/delays overridden-assigns delays nil :rewrite pre-simplify)) (states (svex-alist-keys next-states)) (initst (if initial-state-vars (make-fast-alist (pairlis$ states (svarlist-svex-vars states))) (make-fast-alist (pairlis$ states (replicate (len states) (svex-quote (4vec-x))))))) (in-vars (hons-set-diff (cwtime (svexlist-collect-vars (append (svex-alist-vals updates) (svex-alist-vals next-states))) :mintime 1) (append (svex-alist-keys updates) states))) (updates-for-outs (with-fast-alist updates (make-fast-alist (svex-alist-compose orig-assigns updates)))) (- (fast-alist-free updates) (clear-memoize-table 'svex-compose)) ((mv outexprs final-state all-states) (if keep-all-states (cwtime (svtv-compile 0 nphases ins ovlines outs initst updates-for-outs next-states in-vars keep-final-state t) :mintime 1) (b* (((mv outexprs final-state) (cwtime (svtv-compile-lazy nphases ins ovlines outs initst updates-for-outs next-states in-vars keep-final-state) :mintime 1))) (mv outexprs final-state nil)))) (has-duplicate-outputs (hons-dups-p (svex-alist-keys outexprs))) ((when has-duplicate-outputs) (raise "Duplicated output variable: ~x0" (car has-duplicate-outputs)) (mv nil moddb aliases)) ((mv outexprs final-state) (svtv-simplify-outs/states outexprs final-state simplify)) (inmasks (fast-alist-free (fast-alist-clean (svtv-collect-masks ins)))) (override-inmasks (fast-alist-free (fast-alist-clean (svtv-collect-masks overrides)))) (outmasks (fast-alist-free (fast-alist-clean (svtv-collect-masks outs)))) (inmap (svtv-collect-inmap nil ins nil)) (inmap (svtv-collect-inmap t overrides inmap))) (fast-alist-free updates-for-outs) (mv (make-svtv :name name :outexprs outexprs :nextstate final-state :states all-states :inmasks (append inmasks override-inmasks) :outmasks outmasks :inmap inmap :orig-ins orig-ins :orig-overrides orig-overrides :orig-outs orig-outs :orig-internals orig-internals :expanded-ins ins :expanded-overrides overrides :nphases nphases :labels labels :form form) moddb aliases))))
Theorem:
(defthm return-type-of-defsvtv-main (b* ((res (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form))) (iff (svtv-p res) res)) :rule-classes :rewrite)
Theorem:
(defthm defsvtv-main-of-symbol-fix-name (equal (defsvtv-main (acl2::symbol-fix name) ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form)))
Theorem:
(defthm defsvtv-main-symbol-equiv-congruence-on-name (implies (acl2::symbol-equiv name name-equiv) (equal (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name-equiv ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form))) :rule-classes :congruence)
Theorem:
(defthm defsvtv-main-of-true-list-list-fix-ins (equal (defsvtv-main name (true-list-list-fix ins) overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form)))
Theorem:
(defthm defsvtv-main-true-list-list-equiv-congruence-on-ins (implies (true-list-list-equiv ins ins-equiv) (equal (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins-equiv overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form))) :rule-classes :congruence)
Theorem:
(defthm defsvtv-main-of-true-list-list-fix-overrides (equal (defsvtv-main name ins (true-list-list-fix overrides) outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form)))
Theorem:
(defthm defsvtv-main-true-list-list-equiv-congruence-on-overrides (implies (true-list-list-equiv overrides overrides-equiv) (equal (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides-equiv outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form))) :rule-classes :congruence)
Theorem:
(defthm defsvtv-main-of-true-list-list-fix-outs (equal (defsvtv-main name ins overrides (true-list-list-fix outs) internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form)))
Theorem:
(defthm defsvtv-main-true-list-list-equiv-congruence-on-outs (implies (true-list-list-equiv outs outs-equiv) (equal (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs-equiv internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form))) :rule-classes :congruence)
Theorem:
(defthm defsvtv-main-of-true-list-list-fix-internals (equal (defsvtv-main name ins overrides outs (true-list-list-fix internals) design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form)))
Theorem:
(defthm defsvtv-main-true-list-list-equiv-congruence-on-internals (implies (true-list-list-equiv internals internals-equiv) (equal (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals-equiv design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form))) :rule-classes :congruence)
Theorem:
(defthm defsvtv-main-of-design-fix-design (equal (defsvtv-main name ins overrides outs internals (design-fix design) labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form)))
Theorem:
(defthm defsvtv-main-design-equiv-congruence-on-design (implies (design-equiv design design-equiv) (equal (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design-equiv labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form))) :rule-classes :congruence)
Theorem:
(defthm defsvtv-main-of-symbol-list-fix-labels (equal (defsvtv-main name ins overrides outs internals design (acl2::symbol-list-fix labels) simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form)))
Theorem:
(defthm defsvtv-main-symbol-list-equiv-congruence-on-labels (implies (acl2::symbol-list-equiv labels labels-equiv) (equal (defsvtv-main name ins overrides outs internals design labels simplify pre-simplify initial-state-vars keep-final-state keep-all-states form) (defsvtv-main name ins overrides outs internals design labels-equiv simplify pre-simplify initial-state-vars keep-final-state keep-all-states form))) :rule-classes :congruence)