• Top

• Sv::vl-moddb.lisp

Vl-gate-plainarg-portinfo

Processes a gate instance argument into a vl-portinfo structure.

Signature

(vl-gate-plainarg-portinfo x portname 
                           portdir argindex ss scopes arraysize) 
 
  → 
(mv vttree res)

Arguments

x — Guard (vl-plainarg-p x).

portname — Guard (stringp portname).

portdir — Guard (vl-direction-p portdir).

argindex — Guard (natp argindex).

ss — Guard (vl-scopestack-p ss).

scopes — scopestack where the instance occurs.
    Guard (vl-elabscopes-p scopes).

arraysize — Guard (maybe-posp arraysize).

Returns

vttree — Type (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree)))) .

res — Type (vl-portinfo-p res).

Definitions and Theorems

Function: vl-gate-plainarg-portinfo

(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: return-type-of-vl-gate-plainarg-portinfo.vttree

(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: vl-portinfo-p-of-vl-gate-plainarg-portinfo.res

(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: vars-of-vl-gate-plainarg-portinfo

(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: vl-gate-plainarg-portinfo-of-vl-plainarg-fix-x

(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: vl-gate-plainarg-portinfo-vl-plainarg-equiv-congruence-on-x

(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: vl-gate-plainarg-portinfo-of-str-fix-portname

(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: vl-gate-plainarg-portinfo-streqv-congruence-on-portname

(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: vl-gate-plainarg-portinfo-of-vl-direction-fix-portdir

(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: vl-gate-plainarg-portinfo-vl-direction-equiv-congruence-on-portdir

(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: vl-gate-plainarg-portinfo-of-nfix-argindex

(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: vl-gate-plainarg-portinfo-nat-equiv-congruence-on-argindex

(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: vl-gate-plainarg-portinfo-of-vl-scopestack-fix-ss

(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: vl-gate-plainarg-portinfo-vl-scopestack-equiv-congruence-on-ss

(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: vl-gate-plainarg-portinfo-of-vl-elabscopes-fix-scopes

(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: vl-gate-plainarg-portinfo-vl-elabscopes-equiv-congruence-on-scopes

(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: vl-gate-plainarg-portinfo-of-maybe-posp-fix-arraysize

(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: vl-gate-plainarg-portinfo-maybe-pos-equiv-congruence-on-arraysize

(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)