Processes a gate instance argument into a vl-portinfo structure.
(vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize) → (mv vttree res)
Function:
(defun vl-gate-plainarg-portinfo (x portname portdir argindex ss scopes arraysize) (declare (xargs :guard (and (vl-plainarg-p x) (stringp portname) (vl-direction-p portdir) (natp argindex) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (maybe-posp arraysize)))) (let ((__function__ 'vl-gate-plainarg-portinfo)) (declare (ignorable __function__)) (b* (((fun (fail vttree)) (mv vttree (make-vl-portinfo-bad))) ((vl-plainarg x) (vl-plainarg-fix x)) (portname (string-fix portname)) (arraysize (acl2::maybe-posp-fix arraysize)) (vttree nil) (portexpr (vl-idexpr portname)) (port-lhs (svex-lhs-from-name portname)) (port-type *vl-plain-old-logic-type*) ((unless x.expr) (mv vttree (make-vl-portinfo-regular :portname portname :port-dir (vl-direction-fix portdir) :conn-expr nil :port-lhs port-lhs :conn-svex (sv::svex-z) :port-size 1 :replicatedp (and arraysize t)))) ((vmv vttree x-svex x-type ?x-size type-err) (vl-expr-to-svex-maybe-typed x.expr (if arraysize nil port-type) ss scopes :compattype :equiv)) ((wvmv vttree) (vl-port-type-err-warn portname (vl-direction-fix portdir) x port-type type-err ss scopes)) ((unless x-type) (fail vttree)) ((mv err multi x-size ?port-size) (vl-instarray-plainarg-type-check arraysize port-type portexpr x-type x.expr portname)) ((when err) (fail (vfatal :type :vl-plainarg->svex-fail :msg "~@0" :args (list err)))) (xsvex (sv::svex-concat x-size (sv::svex-lhsrewrite x-svex x-size) (sv::svex-z)))) (mv vttree (make-vl-portinfo-regular :portname portname :port-dir (vl-direction-fix portdir) :conn-expr x.expr :port-lhs port-lhs :conn-svex xsvex :port-size 1 :replicatedp (and arraysize (not multi)))))))
Theorem:
(defthm return-type-of-vl-gate-plainarg-portinfo.vttree (b* (((mv ?vttree ?res) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm vl-portinfo-p-of-vl-gate-plainarg-portinfo.res (b* (((mv ?vttree ?res) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize))) (vl-portinfo-p res)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-gate-plainarg-portinfo (b* (((mv ?vttree ?res) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize))) (sv::svarlist-addr-p (vl-portinfo-vars res))))
Theorem:
(defthm vl-gate-plainarg-portinfo-of-vl-plainarg-fix-x (equal (vl-gate-plainarg-portinfo (vl-plainarg-fix x) portname portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarg-portinfo-vl-plainarg-equiv-congruence-on-x (implies (vl-plainarg-equiv x x-equiv) (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x-equiv portname portdir argindex ss scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarg-portinfo-of-str-fix-portname (equal (vl-gate-plainarg-portinfo x (str-fix portname) portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarg-portinfo-streqv-congruence-on-portname (implies (streqv portname portname-equiv) (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname-equiv portdir argindex ss scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarg-portinfo-of-vl-direction-fix-portdir (equal (vl-gate-plainarg-portinfo x portname (vl-direction-fix portdir) argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarg-portinfo-vl-direction-equiv-congruence-on-portdir (implies (vl-direction-equiv portdir portdir-equiv) (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir-equiv argindex ss scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarg-portinfo-of-nfix-argindex (equal (vl-gate-plainarg-portinfo x portname portdir (nfix argindex) ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarg-portinfo-nat-equiv-congruence-on-argindex (implies (acl2::nat-equiv argindex argindex-equiv) (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex-equiv ss scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarg-portinfo-of-vl-scopestack-fix-ss (equal (vl-gate-plainarg-portinfo x portname portdir argindex (vl-scopestack-fix ss) scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarg-portinfo-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss-equiv scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarg-portinfo-of-vl-elabscopes-fix-scopes (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss (vl-elabscopes-fix scopes) arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarg-portinfo-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes-equiv arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarg-portinfo-of-maybe-posp-fix-arraysize (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes (acl2::maybe-posp-fix arraysize)) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarg-portinfo-maybe-pos-equiv-congruence-on-arraysize (implies (acl2::maybe-pos-equiv arraysize arraysize-equiv) (equal (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize) (vl-gate-plainarg-portinfo x portname portdir argindex ss scopes arraysize-equiv))) :rule-classes :congruence)