Produce the svex wire declaration and any aliases, modinsts, and modules necessary for a given vardecl.
(vl-vardecl->svex x portdecls modalist self-lsb ss scopes config) → (mv vttree width wires fixups aliases modinsts assigns modalist1)
Function:
(defun vl-vardecl->svex (x portdecls modalist self-lsb ss scopes config) (declare (xargs :guard (and (vl-vardecl-p x) (sv::modalist-p modalist) (maybe-natp self-lsb) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (vl-simpconfig-p config)))) (let ((__function__ 'vl-vardecl->svex)) (declare (ignorable __function__)) (b* ((?portdecls portdecls) ((vl-vardecl x) (vl-vardecl-fix x)) (modalist (sv::modalist-fix modalist)) (vttree nil) ((unless (vl-datatype-resolved-p x.type)) (mv (vfatal :type :vl-vardecl->svex-fail :msg "~a0: Failed to resolve usertypes" :args (list x)) 0 nil nil nil nil nil modalist)) ((mv err size) (vl-datatype-size x.type)) ((when (or err (not size))) (mv (vfatal :type :vl-vardecl->svex-fail :msg "~a0: Failed to size datatype ~a1: ~@2" :args (list x x.type (if err err "exact error unknown"))) 0 nil nil nil nil nil modalist)) ((mv err subwire datamod modalist) (vl-datatype->mods x.type modalist)) ((when err) (mv (vfatal :type :vl-vardecl->svex-fail :msg "~a0: Failed to process datatype ~a1: ~@2" :args (list x x.type err)) 0 nil nil nil nil nil modalist)) ((vmv vttree) (vl-vardecl-enum-constraint x portdecls config)) (fixups (vl-vardecl-enum-fixup x portdecls config)) ((mv atts warnings) (vl-atts->svex x.atts (vl-simpconfig->sv-include-atts config) ss scopes)) ((vmv vttree) (vttree-warnings warnings)) ((mv wire insts aliases) (vl-datatype-elem->mod-components x.name subwire self-lsb datamod)) ((sv::wire wire) (sv::change-wire wire :atts atts)) (assigns (cond (x.constval (list (cons (sv::make-simple-lhs :width wire.width :var (sv::make-simple-svar wire.name)) (sv::make-driver :value (sv::svex-quote x.constval) :strength 7)))) ((eq x.nettype :vl-supply0) (list (cons (sv::make-simple-lhs :width wire.width :var (sv::make-simple-svar wire.name)) (sv::make-driver :value (svex-int 0) :strength 7)))) ((eq x.nettype :vl-supply1) (list (cons (sv::make-simple-lhs :width wire.width :var (sv::make-simple-svar wire.name)) (sv::make-driver :value (svex-int (1- (ash 1 wire.width))) :strength 7))))))) (mv vttree size (list wire) fixups aliases insts assigns modalist))))
Theorem:
(defthm return-type-of-vl-vardecl->svex.vttree (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm natp-of-vl-vardecl->svex.width (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (natp width)) :rule-classes :type-prescription)
Theorem:
(defthm wirelist-p-of-vl-vardecl->svex.wires (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-vardecl->svex.fixups (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::assigns-p fixups)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-vardecl->svex.aliases (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-vardecl->svex.modinsts (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::modinstlist-p modinsts)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-vardecl->svex.assigns (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm modalist-p-of-vl-vardecl->svex.modalist1 (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::modalist-p modalist1)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-vardecl->svex-modalist (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (implies (sv::svarlist-addr-p (sv::modalist-vars modalist)) (sv::svarlist-addr-p (sv::modalist-vars modalist1)))))
Theorem:
(defthm vars-of-vl-vardecl->svex-aliases (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))
Theorem:
(defthm vars-of-vl-vardecl->svex-fixups (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::svarlist-addr-p (sv::assigns-vars fixups))))
Theorem:
(defthm vars-of-vl-vardecl->svex-assigns (b* (((mv ?vttree ?width ?wires ?fixups ?aliases ?modinsts ?assigns ?modalist1) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config))) (sv::svarlist-addr-p (sv::assigns-vars assigns))))
Theorem:
(defthm vl-vardecl->svex-of-vl-vardecl-fix-x (equal (vl-vardecl->svex (vl-vardecl-fix x) portdecls modalist self-lsb ss scopes config) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config)))
Theorem:
(defthm vl-vardecl->svex-vl-vardecl-equiv-congruence-on-x (implies (vl-vardecl-equiv x x-equiv) (equal (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config) (vl-vardecl->svex x-equiv portdecls modalist self-lsb ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecl->svex-of-modalist-fix-modalist (equal (vl-vardecl->svex x portdecls (sv::modalist-fix modalist) self-lsb ss scopes config) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config)))
Theorem:
(defthm vl-vardecl->svex-modalist-equiv-congruence-on-modalist (implies (sv::modalist-equiv modalist modalist-equiv) (equal (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config) (vl-vardecl->svex x portdecls modalist-equiv self-lsb ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecl->svex-of-maybe-natp-fix-self-lsb (equal (vl-vardecl->svex x portdecls modalist (maybe-natp-fix self-lsb) ss scopes config) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config)))
Theorem:
(defthm vl-vardecl->svex-maybe-nat-equiv-congruence-on-self-lsb (implies (acl2::maybe-nat-equiv self-lsb self-lsb-equiv) (equal (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config) (vl-vardecl->svex x portdecls modalist self-lsb-equiv ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecl->svex-of-vl-scopestack-fix-ss (equal (vl-vardecl->svex x portdecls modalist self-lsb (vl-scopestack-fix ss) scopes config) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config)))
Theorem:
(defthm vl-vardecl->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config) (vl-vardecl->svex x portdecls modalist self-lsb ss-equiv scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecl->svex-of-vl-elabscopes-fix-scopes (equal (vl-vardecl->svex x portdecls modalist self-lsb ss (vl-elabscopes-fix scopes) config) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config)))
Theorem:
(defthm vl-vardecl->svex-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes-equiv config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecl->svex-of-vl-simpconfig-fix-config (equal (vl-vardecl->svex x portdecls modalist self-lsb ss scopes (vl-simpconfig-fix config)) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config)))
Theorem:
(defthm vl-vardecl->svex-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config) (vl-vardecl->svex x portdecls modalist self-lsb ss scopes config-equiv))) :rule-classes :congruence)