Produces the wires and aliases for an interface instantiation.
(vl-interfaceinst->svex name ifname context ss self-lsb arraywidth) → (mv warnings wires aliases width single-width)
This may be used either for an interface port or for an interface instance. It looks up the instantiated interface and computes its size, producing a wire of that size (named after the instance or port name) and aliases that wire to instname.self. (An appropriate modinst should be constructed separately.)
Function:
(defun vl-interfaceinst->svex (name ifname context ss self-lsb arraywidth) (declare (xargs :guard (and (stringp name) (stringp ifname) (anyp context) (vl-scopestack-p ss) (maybe-natp self-lsb) (maybe-posp arraywidth)))) (let ((__function__ 'vl-interfaceinst->svex)) (declare (ignorable __function__)) (b* ((warnings nil) (ifname (string-fix ifname)) (name (string-fix name)) (arraywidth (acl2::maybe-posp-fix arraywidth)) ((mv iface i-ss) (vl-scopestack-find-definition/ss ifname ss)) ((unless (and iface (eq (tag iface) :vl-interface))) (mv (fatal :type :vl-module->svex-fail :msg "~a0: Interface not found: ~s1" :args (list context ifname)) nil nil 0 0)) ((mv err size) (vl-interface-size iface i-ss)) (warnings (vl-err->fatal err :type :vl-interface->svex-fail :msg "Failed to resolve the size of ~a0" :args (list ifname))) ((unless (posp size)) (mv warnings nil nil 0 0)) (arraysize (if arraywidth (* arraywidth size) size)) (wire (sv::make-wire :name name :width arraysize :low-idx 0)) (aliases (vlsv-aggregate-aliases name arraysize self-lsb))) (mv (ok) (list wire) aliases arraysize size))))
Theorem:
(defthm vl-warninglist-p-of-vl-interfaceinst->svex.warnings (b* (((mv ?warnings ?wires ?aliases ?width ?single-width) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm wirelist-p-of-vl-interfaceinst->svex.wires (b* (((mv ?warnings ?wires ?aliases ?width ?single-width) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-interfaceinst->svex.aliases (b* (((mv ?warnings ?wires ?aliases ?width ?single-width) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-vl-interfaceinst->svex.width (b* (((mv ?warnings ?wires ?aliases ?width ?single-width) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth))) (natp width)) :rule-classes :type-prescription)
Theorem:
(defthm natp-of-vl-interfaceinst->svex.single-width (b* (((mv ?warnings ?wires ?aliases ?width ?single-width) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth))) (natp single-width)) :rule-classes :type-prescription)
Theorem:
(defthm vars-of-vl-interfaceinst->svex (b* (((mv ?warnings ?wires ?aliases ?width ?single-width) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth))) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))
Theorem:
(defthm vl-interfaceinst->svex-of-str-fix-name (equal (vl-interfaceinst->svex (str-fix name) ifname context ss self-lsb arraywidth) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth)))
Theorem:
(defthm vl-interfaceinst->svex-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth) (vl-interfaceinst->svex name-equiv ifname context ss self-lsb arraywidth))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceinst->svex-of-str-fix-ifname (equal (vl-interfaceinst->svex name (str-fix ifname) context ss self-lsb arraywidth) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth)))
Theorem:
(defthm vl-interfaceinst->svex-streqv-congruence-on-ifname (implies (streqv ifname ifname-equiv) (equal (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth) (vl-interfaceinst->svex name ifname-equiv context ss self-lsb arraywidth))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceinst->svex-of-vl-scopestack-fix-ss (equal (vl-interfaceinst->svex name ifname context (vl-scopestack-fix ss) self-lsb arraywidth) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth)))
Theorem:
(defthm vl-interfaceinst->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth) (vl-interfaceinst->svex name ifname context ss-equiv self-lsb arraywidth))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceinst->svex-of-maybe-natp-fix-self-lsb (equal (vl-interfaceinst->svex name ifname context ss (maybe-natp-fix self-lsb) arraywidth) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth)))
Theorem:
(defthm vl-interfaceinst->svex-maybe-nat-equiv-congruence-on-self-lsb (implies (acl2::maybe-nat-equiv self-lsb self-lsb-equiv) (equal (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth) (vl-interfaceinst->svex name ifname context ss self-lsb-equiv arraywidth))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceinst->svex-of-maybe-posp-fix-arraywidth (equal (vl-interfaceinst->svex name ifname context ss self-lsb (acl2::maybe-posp-fix arraywidth)) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth)))
Theorem:
(defthm vl-interfaceinst->svex-maybe-pos-equiv-congruence-on-arraywidth (implies (acl2::maybe-pos-equiv arraywidth arraywidth-equiv) (equal (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth) (vl-interfaceinst->svex name ifname context ss self-lsb arraywidth-equiv))) :rule-classes :congruence)