Processes a module instance argument into a vl-portinfo structure.
(vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) → (mv vttree res)
Function:
(defun vl-plainarg-portinfo (x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (declare (xargs :guard (and (vl-plainarg-p x) (vl-port-p y) (natp argindex) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (stringp inst-modname) (vl-scopestack-p inst-ss) (vl-elabscopes-p inst-scopes) (maybe-posp arraysize)))) (let ((__function__ 'vl-plainarg-portinfo)) (declare (ignorable __function__)) (b* (((fun (fail vttree)) (mv vttree (make-vl-portinfo-bad))) ((vl-plainarg x) (vl-plainarg-fix x)) (y (vl-port-fix y)) (arraysize (acl2::maybe-posp-fix arraysize)) (?inst-modname (string-fix inst-modname)) (vttree nil) ((when (eq (tag y) :vl-interfaceport)) (b* (((unless x.expr) (mv vttree (make-vl-portinfo-bad))) ((vl-interfaceport y)) ((when (and (consp y.udims) (or (consp (cdr y.udims)) (b* ((dim (car y.udims))) (vl-dimension-case dim :range (not (vl-range-resolved-p dim.range)) :otherwise t))))) (fail (vfatal :type :vl-plainarg->svex-fail :msg "Can't handle dimensions of interface port ~a0" :args (list y)))) ((mv err y-memb) (vl-interfaceport-mockmember y inst-ss :reclimit 100)) ((when (or err (not (vl-datatype-resolved-p (vl-structmember->type y-memb))))) (fail (vfatal :type :vl-plainarg->svex-fail :msg "Couldn't get mocktype for interfaceport ~a0: ~@1" :args (list y (or err "not resolved"))))) (y-type (vl-structmember->type y-memb)) ((unless (vl-expr-case x.expr :vl-index)) (fail (vfatal :type :vl-plainarg->svex-fail :msg "Interface port ~a0 connected to non-index arg ~a1" :args (list y x)))) ((vmv vttree x-svex x-type) (vl-index-expr-to-svex x.expr ss scopes)) ((unless (and x-type (vl-datatype-resolved-p x-type))) (fail (vfatal :type :vl-plainarg->svex-fail :msg "Couldn't resolve type for interfaceport argument .~s0(~a1) (type: ~a2)" :args (list y.name x.expr x-type)))) (y-expr (make-vl-index :scope (vl-idscope y.name) :part (if (consp y.udims) (vl-range->partselect (vl-dimension->range (car y.udims))) (vl-partselect-none)))) ((mv type-err multi x-size y-size) (vl-instarray-plainarg-type-check arraysize y-type y-expr x-type x.expr y.name)) (type-err (or type-err (and (not arraysize) (vl-check-datatype-compatibility x-type y-type :equiv)))) ((when type-err) (fail (vfatal :type :vl-plainarg->svex-fail :msg "Types mismatch on interfaceport argument .~s0(~a1): ~@2" :args (list y.name x.expr type-err)))) (y-lhs (svex-lhs-from-name y.name :width y-size)) (xsvex (sv::svex-concat x-size (sv::svex-lhsrewrite x-svex x-size) (sv::svex-z)))) (mv vttree (make-vl-portinfo-regular :portname y.name :port-dir nil :conn-expr x.expr :port-lhs y-lhs :conn-svex xsvex :port-size y-size :replicatedp (and arraysize (not multi)) :interfacep t)))) ((vl-regularport y)) (y.name (or y.name (cat "unnamed_port_" (natstr argindex)))) (vttree nil) ((unless (or y.expr x.expr)) (mv vttree (make-vl-portinfo-regular :portname y.name :port-dir x.dir :conn-expr nil :port-lhs nil :conn-svex (sv::svex-z) :port-size 1 :replicatedp (and arraysize t)))) ((vmv vttree y-lhs y-type) (if y.expr (vl-expr-to-svex-lhs y.expr inst-ss inst-scopes) (mv vttree nil nil))) ((unless (or (not y.expr) y-type)) (fail vttree)) ((unless x.expr) (b* (((mv err y-size) (vl-datatype-size y-type)) ((when (or err (not y-size) (eql 0 y-size))) (fail (vfatal :type :vl-plainarg->svex-fail :msg "~@0" :args (list (vmsg "Couldn't size datatype ~a0 for ~s1 port expression ~a2" (vl-datatype-fix y-type) (string-fix y.name) (vl-expr-fix y.expr))))))) (mv vttree (make-vl-portinfo-regular :portname y.name :port-dir x.dir :conn-expr nil :port-lhs y-lhs :conn-svex (sv::svex-z) :port-size y-size :replicatedp (and arraysize t))))) ((vmv vttree x-svex x-type ?x-size type-err) (b* ((type-to-use (and (not arraysize) (or (not (eq x.dir :vl-output)) (vl-expr-needs-type-context x.expr) (and y-type (not (vl-datatype-packedp y-type)))) y-type))) (vl-expr-to-svex-maybe-typed x.expr type-to-use ss scopes :compattype :assign))) ((unless y.expr) (mv vttree (make-vl-portinfo-regular :portname y.name :port-dir x.dir :conn-expr x.expr :port-lhs nil :conn-svex x-svex :port-size 1 :replicatedp (and arraysize t)))) ((wvmv vttree) (vl-port-type-err-warn y.name x.dir x y-type type-err ss scopes)) ((unless x-type) (fail vttree)) ((mv err ?multi ?x-size ?y-size) (vl-instarray-plainarg-type-check arraysize y-type y.expr x-type x.expr y.name)) ((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 y.name :port-dir x.dir :conn-expr x.expr :port-lhs y-lhs :conn-svex xsvex :port-size y-size :replicatedp (and arraysize (not multi)))))))
Theorem:
(defthm return-type-of-vl-plainarg-portinfo.vttree (b* (((mv ?vttree ?res) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-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-plainarg-portinfo.res (b* (((mv ?vttree ?res) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize))) (vl-portinfo-p res)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-plainarg-portinfo (b* (((mv ?vttree ?res) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize))) (and (sv::svarlist-addr-p (vl-portinfo-vars res)))))
Theorem:
(defthm vl-plainarg-portinfo-of-vl-plainarg-fix-x (equal (vl-plainarg-portinfo (vl-plainarg-fix x) y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-vl-plainarg-equiv-congruence-on-x (implies (vl-plainarg-equiv x x-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x-equiv y argindex ss scopes inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-portinfo-of-vl-port-fix-y (equal (vl-plainarg-portinfo x (vl-port-fix y) argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-vl-port-equiv-congruence-on-y (implies (vl-port-equiv y y-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y-equiv argindex ss scopes inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-portinfo-of-nfix-argindex (equal (vl-plainarg-portinfo x y (nfix argindex) ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-nat-equiv-congruence-on-argindex (implies (acl2::nat-equiv argindex argindex-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex-equiv ss scopes inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-portinfo-of-vl-scopestack-fix-ss (equal (vl-plainarg-portinfo x y argindex (vl-scopestack-fix ss) scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss-equiv scopes inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-portinfo-of-vl-elabscopes-fix-scopes (equal (vl-plainarg-portinfo x y argindex ss (vl-elabscopes-fix scopes) inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes-equiv inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-portinfo-of-str-fix-inst-modname (equal (vl-plainarg-portinfo x y argindex ss scopes (str-fix inst-modname) inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-streqv-congruence-on-inst-modname (implies (streqv inst-modname inst-modname-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname-equiv inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-portinfo-of-vl-scopestack-fix-inst-ss (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname (vl-scopestack-fix inst-ss) inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-vl-scopestack-equiv-congruence-on-inst-ss (implies (vl-scopestack-equiv inst-ss inst-ss-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss-equiv inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-portinfo-of-vl-elabscopes-fix-inst-scopes (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss (vl-elabscopes-fix inst-scopes) arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-vl-elabscopes-equiv-congruence-on-inst-scopes (implies (vl-elabscopes-equiv inst-scopes inst-scopes-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes-equiv arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarg-portinfo-of-maybe-posp-fix-arraysize (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes (acl2::maybe-posp-fix arraysize)) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarg-portinfo-maybe-pos-equiv-congruence-on-arraysize (implies (acl2::maybe-pos-equiv arraysize arraysize-equiv) (equal (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarg-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize-equiv))) :rule-classes :congruence)