Translate a combinational or latch-type always block into a set of SVEX expressions.
(vl-alwayslist->svex x ss scopes config) → (mv warnings assigns constraints)
Function:
(defun vl-alwayslist->svex (x ss scopes config) (declare (xargs :guard (and (vl-alwayslist-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (vl-simpconfig-p config)))) (let ((__function__ 'vl-alwayslist->svex)) (declare (ignorable __function__)) (b* ((warnings nil) ((when (atom x)) (mv (ok) nil nil)) ((wmv warnings assigns1 constraints1) (time$ (vl-always->svex (car x) ss scopes config) :mintime 1 :msg "; vl-always->svex at ~s0 total: ~st sec, ~sa bytes~%" :args (list (vl-location-string (vl-always->loc (car x)))))) ((wmv warnings assigns2 constraints2) (vl-alwayslist->svex (cdr x) ss scopes config))) (mv warnings (append-without-guard assigns1 assigns2) (append-without-guard constraints1 constraints2)))))
Theorem:
(defthm vl-warninglist-p-of-vl-alwayslist->svex.warnings (b* (((mv ?warnings ?assigns ?constraints) (vl-alwayslist->svex x ss scopes config))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-alwayslist->svex.assigns (b* (((mv ?warnings ?assigns ?constraints) (vl-alwayslist->svex x ss scopes config))) (sv::assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm constraintlist-p-of-vl-alwayslist->svex.constraints (b* (((mv ?warnings ?assigns ?constraints) (vl-alwayslist->svex x ss scopes config))) (sv::constraintlist-p constraints)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-alwayslist->svex (b* (((mv ?warnings ?assigns ?constraints) (vl-alwayslist->svex x ss scopes config))) (and (sv::svarlist-addr-p (sv::assigns-vars assigns)) (sv::svarlist-addr-p (sv::constraintlist-vars constraints)))))
Theorem:
(defthm vl-alwayslist->svex-of-vl-alwayslist-fix-x (equal (vl-alwayslist->svex (vl-alwayslist-fix x) ss scopes config) (vl-alwayslist->svex x ss scopes config)))
Theorem:
(defthm vl-alwayslist->svex-vl-alwayslist-equiv-congruence-on-x (implies (vl-alwayslist-equiv x x-equiv) (equal (vl-alwayslist->svex x ss scopes config) (vl-alwayslist->svex x-equiv ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-alwayslist->svex-of-vl-scopestack-fix-ss (equal (vl-alwayslist->svex x (vl-scopestack-fix ss) scopes config) (vl-alwayslist->svex x ss scopes config)))
Theorem:
(defthm vl-alwayslist->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-alwayslist->svex x ss scopes config) (vl-alwayslist->svex x ss-equiv scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-alwayslist->svex-of-vl-elabscopes-fix-scopes (equal (vl-alwayslist->svex x ss (vl-elabscopes-fix scopes) config) (vl-alwayslist->svex x ss scopes config)))
Theorem:
(defthm vl-alwayslist->svex-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-alwayslist->svex x ss scopes config) (vl-alwayslist->svex x ss scopes-equiv config))) :rule-classes :congruence)
Theorem:
(defthm vl-alwayslist->svex-of-vl-simpconfig-fix-config (equal (vl-alwayslist->svex x ss scopes (vl-simpconfig-fix config)) (vl-alwayslist->svex x ss scopes config)))
Theorem:
(defthm vl-alwayslist->svex-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-alwayslist->svex x ss scopes config) (vl-alwayslist->svex x ss scopes config-equiv))) :rule-classes :congruence)