Produces all the new svex module components associated with a VL module instance or instance array.
(vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) → (mv vttree wires assigns1 aliases1 width modinsts modalist)
See vl-hierarchy-sv-translation for more information on how VL module instances are translated.
Function:
(defun vl-modinst->svex-assigns/aliases (x ss scopes wires assigns aliases context-mod self-lsb) (declare (xargs :guard (and (vl-modinst-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-modinst->svex-assigns/aliases)) (declare (ignorable __function__)) (b* (((vl-modinst x) (vl-modinst-fix x)) (wires (sv::wirelist-fix wires)) (assigns (sv::assigns-fix assigns)) (aliases (sv::lhspairs-fix aliases)) (context-mod (sv::modname-fix context-mod)) (vttree nil) ((when (eq (vl-arguments-kind x.portargs) :vl-arguments-named)) (mv (vfatal :type :vl-modinst->svex-fail :msg "~a0: Unexpectedly had named arglist" :args (list x)) wires assigns aliases 0 nil nil)) (x.plainargs (vl-arguments->args x.portargs)) ((mv inst-mod inst-ss) (vl-scopestack-find-definition/ss x.modname ss)) ((unless (and inst-mod (or (eq (tag inst-mod) :vl-module) (eq (tag inst-mod) :vl-interface)))) (mv (vfatal :type :vl-modinst->svex-fail :msg "~a0: Unknown module ~s1" :args (list x x.modname)) wires assigns aliases 0 nil nil)) (inst-ss (vl-scopestack-push inst-mod inst-ss)) (inst-scopes (vl-elabscopes-push-scope inst-mod (vl-elabscopes-root scopes))) (i.ports (if (eq (tag inst-mod) :vl-module) (vl-module->ports inst-mod) (vl-interface->ports inst-mod))) (inst-modname (if (eq (tag inst-mod) :vl-module) (vl-module->name inst-mod) (vl-interface->name inst-mod))) ((unless (eql (len i.ports) (len x.plainargs))) (mv (vfatal :type :vl-modinst->svex-fail :msg "~a0: Mismatched portlist length" :args (list x)) wires assigns aliases 0 nil nil)) ((unless (vl-maybe-range-resolved-p x.range)) (mv (vfatal :type :vl-modinst->svex-fail :msg "~a0: Unresolved instance array range" :args (list x)) wires assigns aliases 0 nil nil)) (arraywidth (and x.range (vl-range-size x.range))) ((unless x.instname) (mv (vfatal :type :vl-modinst->svex-fail :msg "~a0: Unnamed module/interface instance not allowed" :args (list x)) wires assigns aliases 0 nil nil)) ((vmv vttree portinfo :ctx x) (vl-plainarglist-portinfo x.plainargs i.ports 0 ss scopes inst-modname inst-ss inst-scopes arraywidth)) ((wvmv vttree portassigns portaliases :ctx x) (vl-portinfolist-to-svex-assigns/aliases portinfo x.instname x.range)) (assigns (append-without-guard portassigns assigns)) (aliases (append-without-guard portaliases aliases)) ((wvmv vttree ifwires ifaliases arrwidth iface-width :ctx x) (if (eq (tag inst-mod) :vl-interface) (vl-interfaceinst->svex x.instname x.modname x ss self-lsb arraywidth) (mv nil nil nil 0 nil))) (wires (append-without-guard ifwires wires)) (aliases (append-without-guard ifaliases aliases)) ((unless arraywidth) (mv (make-vttree-context :ctx x :subtree vttree) wires assigns aliases arrwidth (list (sv::make-modinst :instname x.instname :modname x.modname)) nil)) (array-modname (list :arraymod context-mod x.instname)) (modinst (sv::make-modinst :instname x.instname :modname array-modname)) ((mv arraymod-aliases arraymod-modinsts arraymod-ifacewires) (vl-instarray-nested-aliases portinfo (vl-range-msbidx x.range) arraywidth (if (vl-range-revp x.range) 1 -1) inst-modname iface-width)) (arraymod-selfwire (and (eq (tag inst-mod) :vl-interface) (posp arrwidth) (list (sv::make-wire :name :self :width arrwidth :low-idx 0)))) (arraymod (sv::make-module :wires (append arraymod-selfwire arraymod-ifacewires) :insts arraymod-modinsts :aliaspairs arraymod-aliases))) (mv (make-vttree-context :ctx x :subtree vttree) wires assigns aliases arrwidth (list modinst) (list (cons array-modname arraymod))))))
Theorem:
(defthm return-type-of-vl-modinst->svex-assigns/aliases.vttree (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->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-modinst->svex-assigns/aliases.wires (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-modinst->svex-assigns/aliases.assigns1 (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->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-modinst->svex-assigns/aliases.aliases1 (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->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-modinst->svex-assigns/aliases.width (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->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-modinst->svex-assigns/aliases.modinsts (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->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-modinst->svex-assigns/aliases.modalist (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->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-modinst->svex-assigns/aliases-assigns (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->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-modinst->svex-assigns/aliases-aliases (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->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-modinst->svex-assigns/aliases-modalist (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?width ?modinsts ?modalist) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb))) (sv::svarlist-addr-p (sv::modalist-vars modalist))))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-of-vl-modinst-fix-x (equal (vl-modinst->svex-assigns/aliases (vl-modinst-fix x) ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-vl-modinst-equiv-congruence-on-x (implies (vl-modinst-equiv x x-equiv) (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x-equiv ss scopes wires assigns aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst->svex-assigns/aliases-of-vl-scopestack-fix-ss (equal (vl-modinst->svex-assigns/aliases x (vl-scopestack-fix ss) scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss-equiv scopes wires assigns aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst->svex-assigns/aliases-of-vl-elabscopes-fix-scopes (equal (vl-modinst->svex-assigns/aliases x ss (vl-elabscopes-fix scopes) wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes-equiv wires assigns aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst->svex-assigns/aliases-of-wirelist-fix-wires (equal (vl-modinst->svex-assigns/aliases x ss scopes (sv::wirelist-fix wires) assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-wirelist-equiv-congruence-on-wires (implies (sv::wirelist-equiv wires wires-equiv) (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires-equiv assigns aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst->svex-assigns/aliases-of-assigns-fix-assigns (equal (vl-modinst->svex-assigns/aliases x ss scopes wires (sv::assigns-fix assigns) aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-assigns-equiv-congruence-on-assigns (implies (sv::assigns-equiv assigns assigns-equiv) (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns-equiv aliases context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst->svex-assigns/aliases-of-lhspairs-fix-aliases (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns (sv::lhspairs-fix aliases) context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-lhspairs-equiv-congruence-on-aliases (implies (sv::lhspairs-equiv aliases aliases-equiv) (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases-equiv context-mod self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst->svex-assigns/aliases-of-modname-fix-context-mod (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases (sv::modname-fix context-mod) self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-modname-equiv-congruence-on-context-mod (implies (sv::modname-equiv context-mod context-mod-equiv) (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod-equiv self-lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-modinst->svex-assigns/aliases-of-maybe-natp-fix-self-lsb (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod (maybe-natp-fix self-lsb)) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb)))
Theorem:
(defthm vl-modinst->svex-assigns/aliases-maybe-nat-equiv-congruence-on-self-lsb (implies (acl2::maybe-nat-equiv self-lsb self-lsb-equiv) (equal (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) (vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb-equiv))) :rule-classes :congruence)