Produces svex wires, insts, aliases for an interface port.
(vl-interfaceport->svex x ss self-lsb context-mod) → (mv warnings wires insts aliases modalist width)
Just adds a modinst to the outputs of vl-interfaceinst->svex.
Function:
(defun vl-interfaceport->svex (x ss self-lsb context-mod) (declare (xargs :guard (and (vl-interfaceport-p x) (vl-scopestack-p ss) (maybe-natp self-lsb) (sv::modname-p context-mod)))) (let ((__function__ 'vl-interfaceport->svex)) (declare (ignorable __function__)) (b* (((vl-interfaceport x) (vl-interfaceport-fix x)) (context-mod (sv::modname-fix context-mod)) (warnings nil) ((unless (or (atom x.udims) (and (atom (cdr x.udims)) (vl-dimension-case (car x.udims) :range) (vl-range-resolved-p (vl-dimension->range (car x.udims)))))) (mv (fatal :type :vl-bad-interfaceport-array :msg "Unresolved or unsized dimensions on interfaceport array: ~a0" :args (list x)) nil nil nil nil 0)) (range (and (consp x.udims) (vl-dimension->range (car x.udims)))) (arraysize (and range (vl-range-size range))) ((wmv warnings wires aliases arrwidth singlewidth) (vl-interfaceinst->svex x.name x.ifname x ss self-lsb arraysize)) ((unless (and arraysize (posp arrwidth))) (mv warnings wires (list (sv::make-modinst :instname x.name :modname x.ifname)) aliases nil arrwidth)) ((mv arraymod-aliases arraymod-modinsts arraymod-ifacewires) (vl-instarray-nested-aliases nil (vl-resolved->val (vl-range->msb range)) arraysize (if (vl-range-revp range) 1 -1) x.ifname singlewidth)) (arraymod-selfwire (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)) (array-modname (list :array-ifportmod context-mod x.name)) (insts (list (sv::make-modinst :instname x.name :modname array-modname)))) (mv warnings wires insts aliases (list (cons array-modname arraymod)) arrwidth))))
Theorem:
(defthm vl-warninglist-p-of-vl-interfaceport->svex.warnings (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceport->svex x ss self-lsb context-mod))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm wirelist-p-of-vl-interfaceport->svex.wires (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceport->svex x ss self-lsb context-mod))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-interfaceport->svex.insts (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceport->svex x ss self-lsb context-mod))) (sv::modinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-interfaceport->svex.aliases (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceport->svex x ss self-lsb context-mod))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm modalist-p-of-vl-interfaceport->svex.modalist (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceport->svex x ss self-lsb context-mod))) (sv::modalist-p modalist)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-vl-interfaceport->svex.width (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceport->svex x ss self-lsb context-mod))) (natp width)) :rule-classes :type-prescription)
Theorem:
(defthm vars-of-vl-interfaceport->svex (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceport->svex x ss self-lsb context-mod))) (and (sv::svarlist-addr-p (sv::lhspairs-vars aliases)) (sv::svarlist-addr-p (sv::modalist-vars modalist)))))
Theorem:
(defthm vl-interfaceport->svex-of-vl-interfaceport-fix-x (equal (vl-interfaceport->svex (vl-interfaceport-fix x) ss self-lsb context-mod) (vl-interfaceport->svex x ss self-lsb context-mod)))
Theorem:
(defthm vl-interfaceport->svex-vl-interfaceport-equiv-congruence-on-x (implies (vl-interfaceport-equiv x x-equiv) (equal (vl-interfaceport->svex x ss self-lsb context-mod) (vl-interfaceport->svex x-equiv ss self-lsb context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceport->svex-of-vl-scopestack-fix-ss (equal (vl-interfaceport->svex x (vl-scopestack-fix ss) self-lsb context-mod) (vl-interfaceport->svex x ss self-lsb context-mod)))
Theorem:
(defthm vl-interfaceport->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-interfaceport->svex x ss self-lsb context-mod) (vl-interfaceport->svex x ss-equiv self-lsb context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceport->svex-of-maybe-natp-fix-self-lsb (equal (vl-interfaceport->svex x ss (maybe-natp-fix self-lsb) context-mod) (vl-interfaceport->svex x ss self-lsb context-mod)))
Theorem:
(defthm vl-interfaceport->svex-maybe-nat-equiv-congruence-on-self-lsb (implies (acl2::maybe-nat-equiv self-lsb self-lsb-equiv) (equal (vl-interfaceport->svex x ss self-lsb context-mod) (vl-interfaceport->svex x ss self-lsb-equiv context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceport->svex-of-modname-fix-context-mod (equal (vl-interfaceport->svex x ss self-lsb (sv::modname-fix context-mod)) (vl-interfaceport->svex x ss self-lsb context-mod)))
Theorem:
(defthm vl-interfaceport->svex-modname-equiv-congruence-on-context-mod (implies (sv::modname-equiv context-mod context-mod-equiv) (equal (vl-interfaceport->svex x ss self-lsb context-mod) (vl-interfaceport->svex x ss self-lsb context-mod-equiv))) :rule-classes :congruence)