Collects svex module components for a list of module/interface instances, by collecting results from vl-gateinst->svex-assigns/aliases.
(vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) → (mv vttree wires1 assigns1 aliases1 gateinsts modalist)
Function:
(defun vl-gateinstlist->svex-assigns/aliases (x ss scopes wires assigns aliases context-mod) (declare (xargs :guard (and (vl-gateinstlist-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (sv::wirelist-p wires) (sv::assigns-p assigns) (sv::lhspairs-p aliases) (sv::modname-p context-mod)))) (let ((__function__ 'vl-gateinstlist->svex-assigns/aliases)) (declare (ignorable __function__)) (b* ((vttree nil) ((when (atom x)) (mv nil (sv::wirelist-fix wires) (sv::assigns-fix assigns) (sv::lhspairs-fix aliases) nil nil)) ((vmv vttree wires assigns aliases insts1 modalist1) (vl-gateinst->svex-assigns/aliases (car x) ss scopes wires assigns aliases context-mod)) ((vmv vttree wires assigns aliases insts2 modalist2) (vl-gateinstlist->svex-assigns/aliases (cdr x) ss scopes wires assigns aliases context-mod))) (mv vttree wires assigns aliases (append-without-guard insts1 insts2) (append-without-guard modalist1 modalist2)))))
Theorem:
(defthm return-type-of-vl-gateinstlist->svex-assigns/aliases.vttree (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm wirelist-p-of-vl-gateinstlist->svex-assigns/aliases.wires1 (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::wirelist-p wires1)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-gateinstlist->svex-assigns/aliases.assigns1 (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::assigns-p assigns1)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-gateinstlist->svex-assigns/aliases.aliases1 (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::lhspairs-p aliases1)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-gateinstlist->svex-assigns/aliases.gateinsts (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::modinstlist-p gateinsts)) :rule-classes :rewrite)
Theorem:
(defthm modalist-p-of-vl-gateinstlist->svex-assigns/aliases.modalist (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::modalist-p modalist)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-gateinstlist->svex-assigns/aliases-assigns (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (implies (sv::svarlist-addr-p (sv::assigns-vars assigns)) (sv::svarlist-addr-p (sv::assigns-vars assigns1)))))
Theorem:
(defthm vars-of-vl-gateinstlist->svex-assigns/aliases-aliases (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (implies (sv::svarlist-addr-p (sv::lhspairs-vars aliases)) (sv::svarlist-addr-p (sv::lhspairs-vars aliases1)))))
Theorem:
(defthm vars-of-vl-gateinstlist->svex-assigns/aliases-modalist (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?gateinsts ?modalist) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::svarlist-addr-p (sv::modalist-vars modalist))))
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-of-vl-gateinstlist-fix-x (equal (vl-gateinstlist->svex-assigns/aliases (vl-gateinstlist-fix x) ss scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-vl-gateinstlist-equiv-congruence-on-x (implies (vl-gateinstlist-equiv x x-equiv) (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x-equiv ss scopes wires assigns aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-of-vl-scopestack-fix-ss (equal (vl-gateinstlist->svex-assigns/aliases x (vl-scopestack-fix ss) scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss-equiv scopes wires assigns aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-of-vl-elabscopes-fix-scopes (equal (vl-gateinstlist->svex-assigns/aliases x ss (vl-elabscopes-fix scopes) wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes-equiv wires assigns aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-of-wirelist-fix-wires (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes (sv::wirelist-fix wires) assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-wirelist-equiv-congruence-on-wires (implies (sv::wirelist-equiv wires wires-equiv) (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires-equiv assigns aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-of-assigns-fix-assigns (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires (sv::assigns-fix assigns) aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-assigns-equiv-congruence-on-assigns (implies (sv::assigns-equiv assigns assigns-equiv) (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns-equiv aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-of-lhspairs-fix-aliases (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns (sv::lhspairs-fix aliases) context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-lhspairs-equiv-congruence-on-aliases (implies (sv::lhspairs-equiv aliases aliases-equiv) (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases-equiv context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-of-modname-fix-context-mod (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases (sv::modname-fix context-mod)) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinstlist->svex-assigns/aliases-modname-equiv-congruence-on-context-mod (implies (sv::modname-equiv context-mod context-mod-equiv) (equal (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod-equiv))) :rule-classes :congruence)