Collects svex module components for a list of module/interface instances, by collecting results from vl-modinst->svex-assigns/aliases.
(vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) → (mv vttree wires1 assigns1 aliases1 width modinsts modalist)
Function:
(defun vl-modinstlist->svex-assigns/aliases (x ss scopes wires assigns aliases context-mod self-lsb) (declare (xargs :guard (and (vl-modinstlist-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) (maybe-natp self-lsb)))) (let ((__function__ 'vl-modinstlist->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) 0 nil nil)) (self-lsb (maybe-natp-fix self-lsb)) ((vmv vttree wires assigns aliases width2 insts2 modalist2) (vl-modinstlist->svex-assigns/aliases (cdr x) ss scopes wires assigns aliases context-mod self-lsb)) ((vmv vttree wires assigns aliases width1 insts1 modalist1) (vl-modinst->svex-assigns/aliases (car x) ss scopes wires assigns aliases context-mod (and self-lsb (+ self-lsb width2))))) (mv vttree wires assigns aliases (+ width1 width2) (append-without-guard insts1 insts2) (append-without-guard modalist1 modalist2)))))
Theorem:
(defthm return-type-of-vl-modinstlist->svex-assigns/aliases.vttree (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm wirelist-p-of-vl-modinstlist->svex-assigns/aliases.wires1 (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (sv::wirelist-p wires1)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-modinstlist->svex-assigns/aliases.assigns1 (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (sv::assigns-p assigns1)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-modinstlist->svex-assigns/aliases.aliases1 (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (sv::lhspairs-p aliases1)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-vl-modinstlist->svex-assigns/aliases.width (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (natp width)) :rule-classes :type-prescription)
Theorem:
(defthm modinstlist-p-of-vl-modinstlist->svex-assigns/aliases.modinsts (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (sv::modinstlist-p modinsts)) :rule-classes :rewrite)
Theorem:
(defthm modalist-p-of-vl-modinstlist->svex-assigns/aliases.modalist (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (sv::modalist-p modalist)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-modinstlist->svex-assigns/aliases-assigns (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (implies (sv::svarlist-addr-p (sv::assigns-vars assigns)) (sv::svarlist-addr-p (sv::assigns-vars assigns1)))))
Theorem:
(defthm vars-of-vl-modinstlist->svex-assigns/aliases-aliases (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (implies (sv::svarlist-addr-p (sv::lhspairs-vars aliases)) (sv::svarlist-addr-p (sv::lhspairs-vars aliases1)))))
Theorem:
(defthm vars-of-vl-modinstlist->svex-assigns/aliases-modalist (b* (((mv ?vttree ?wires1 ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (sv::svarlist-addr-p (sv::modalist-vars modalist))))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-of-vl-modinstlist-fix-x (equal (vl-modinstlist->svex-assigns/aliases (vl-modinstlist-fix x) ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-vl-modinstlist-equiv-congruence-on-x (implies (vl-modinstlist-equiv x x-equiv) (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x-equiv ss scopes wires assigns aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-of-vl-scopestack-fix-ss (equal (vl-modinstlist->svex-assigns/aliases x (vl-scopestack-fix ss) scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss-equiv scopes wires assigns aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-of-vl-elabscopes-fix-scopes (equal (vl-modinstlist->svex-assigns/aliases x ss (vl-elabscopes-fix scopes) wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes-equiv wires assigns aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-of-wirelist-fix-wires (equal (vl-modinstlist->svex-assigns/aliases x ss scopes (sv::wirelist-fix wires) assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-wirelist-equiv-congruence-on-wires (implies (sv::wirelist-equiv wires wires-equiv) (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires-equiv assigns aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-of-assigns-fix-assigns (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires (sv::assigns-fix assigns) aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-assigns-equiv-congruence-on-assigns (implies (sv::assigns-equiv assigns assigns-equiv) (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns-equiv aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-of-lhspairs-fix-aliases (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns (sv::lhspairs-fix aliases) context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-lhspairs-equiv-congruence-on-aliases (implies (sv::lhspairs-equiv aliases aliases-equiv) (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases-equiv context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-of-modname-fix-context-mod (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases (sv::modname-fix context-mod) self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-modname-equiv-congruence-on-context-mod (implies (sv::modname-equiv context-mod context-mod-equiv) (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod-equiv self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-of-maybe-natp-fix-self-lsb (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod (maybe-natp-fix self-lsb)) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinstlist->svex-assigns/aliases-maybe-nat-equiv-congruence-on-self-lsb (implies (acl2::maybe-nat-equiv self-lsb self-lsb-equiv) (equal (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinstlist->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb-equiv))) :rule-classes :congruence)