Produces all the new svex module components associated with a VL module instance or instance array.
(vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) → (mv vttree wires assigns1 aliases1 modinsts modalist)
See vl-hierarchy-sv-translation for more information on how VL module instances are translated.
Function:
(defun vl-gateinst->svex-assigns/aliases (x ss scopes wires assigns aliases context-mod) (declare (xargs :guard (and (vl-gateinst-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-gateinst->svex-assigns/aliases)) (declare (ignorable __function__)) (b* (((vl-gateinst x) (vl-gateinst-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) (nargs (len x.args)) ((mv err portnames portdirs svex-mod) (vl-gate-make-svex-module x.type nargs)) ((when err) (mv (vfatal :type :vl-gateinst->svex-fail :msg "~a0: bad gate instance: ~@1" :args (list x err)) wires assigns aliases nil nil)) ((unless (vl-maybe-range-resolved-p x.range)) (mv (vfatal :type :vl-gateinst->svex-fail :msg "~a0: Unresolved gate instance array range" :args (list x)) wires assigns aliases nil nil)) (arraywidth (and x.range (vl-range-size x.range))) ((unless x.name) (mv (vfatal :type :vl-gateinst->svex-fail :msg "~a0: Unnamed gate instance not allowed" :args (list x)) wires assigns aliases nil nil)) ((vmv vttree portinfo :ctx x) (vl-gate-plainarglist-portinfo x.args portnames portdirs 0 ss scopes arraywidth)) ((wvmv vttree portassigns portaliases :ctx x) (vl-portinfolist-to-svex-assigns/aliases portinfo x.name x.range)) (assigns (append-without-guard portassigns assigns)) (aliases (append-without-guard portaliases aliases)) (gate-modname (hons-copy (cons ':gate (cons x.type (cons nargs 'nil))))) (modalist (list (cons gate-modname svex-mod))) ((unless arraywidth) (mv (make-vttree-context :ctx x :subtree vttree) wires assigns aliases (list (sv::make-modinst :instname x.name :modname gate-modname)) modalist)) (array-modname (list :arraymod context-mod x.name)) (modinst (sv::make-modinst :instname x.name :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) gate-modname nil)) (arraymod (sv::make-module :wires arraymod-ifacewires :insts arraymod-modinsts :aliaspairs arraymod-aliases))) (mv (make-vttree-context :ctx x :subtree vttree) wires assigns aliases (list modinst) (cons (cons array-modname arraymod) modalist)))))
Theorem:
(defthm return-type-of-vl-gateinst->svex-assigns/aliases.vttree (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->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-gateinst->svex-assigns/aliases.wires (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-gateinst->svex-assigns/aliases.assigns1 (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::assigns-p assigns1)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-gateinst->svex-assigns/aliases.aliases1 (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::lhspairs-p aliases1)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-gateinst->svex-assigns/aliases.modinsts (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::modinstlist-p modinsts)) :rule-classes :rewrite)
Theorem:
(defthm modalist-p-of-vl-gateinst->svex-assigns/aliases.modalist (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::modalist-p modalist)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-gateinst->svex-assigns/aliases-assigns (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->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-gateinst->svex-assigns/aliases-aliases (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->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-gateinst->svex-assigns/aliases-modalist (b* (((mv ?vttree ?wires ?assigns1 ?aliases1 ?modinsts ?modalist) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod))) (sv::svarlist-addr-p (sv::modalist-vars modalist))))
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-of-vl-gateinst-fix-x (equal (vl-gateinst->svex-assigns/aliases (vl-gateinst-fix x) ss scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-vl-gateinst-equiv-congruence-on-x (implies (vl-gateinst-equiv x x-equiv) (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x-equiv ss scopes wires assigns aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-of-vl-scopestack-fix-ss (equal (vl-gateinst->svex-assigns/aliases x (vl-scopestack-fix ss) scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss-equiv scopes wires assigns aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-of-vl-elabscopes-fix-scopes (equal (vl-gateinst->svex-assigns/aliases x ss (vl-elabscopes-fix scopes) wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes-equiv wires assigns aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-of-wirelist-fix-wires (equal (vl-gateinst->svex-assigns/aliases x ss scopes (sv::wirelist-fix wires) assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-wirelist-equiv-congruence-on-wires (implies (sv::wirelist-equiv wires wires-equiv) (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires-equiv assigns aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-of-assigns-fix-assigns (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires (sv::assigns-fix assigns) aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-assigns-equiv-congruence-on-assigns (implies (sv::assigns-equiv assigns assigns-equiv) (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns-equiv aliases context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-of-lhspairs-fix-aliases (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns (sv::lhspairs-fix aliases) context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-lhspairs-equiv-congruence-on-aliases (implies (sv::lhspairs-equiv aliases aliases-equiv) (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases-equiv context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-of-modname-fix-context-mod (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases (sv::modname-fix context-mod)) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod)))
Theorem:
(defthm vl-gateinst->svex-assigns/aliases-modname-equiv-congruence-on-context-mod (implies (sv::modname-equiv context-mod context-mod-equiv) (equal (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod) (vl-gateinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod-equiv))) :rule-classes :congruence)