• Top

• Sv::vl-moddb.lisp

Vl-interfaceinst->svex

Produces the wires and aliases for an interface instantiation.

Signature

(vl-interfaceinst->svex name ifname context ss self-lsb arraywidth) 
  → 
(mv warnings wires aliases width single-width)

Arguments

name — name of instance or interface port.
    Guard (stringp name).

ifname — name of the interface.
    Guard (stringp ifname).

context — Guard (anyp context).

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

self-lsb — indicates we're inside an interface and should make an additional alias to the outer block starting at self-lsb.
    Guard (maybe-natp self-lsb).

arraywidth — indicates an array of instances.
    Guard (maybe-posp arraywidth).

Returns

warnings — Type (vl-warninglist-p warnings).

wires — Type (sv::wirelist-p wires).

aliases — Type (sv::lhspairs-p aliases).

width — Type (natp width).

single-width — Type (natp 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.)

Definitions and Theorems

Function: vl-interfaceinst->svex

(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: vl-warninglist-p-of-vl-interfaceinst->svex.warnings

(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: wirelist-p-of-vl-interfaceinst->svex.wires

(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: lhspairs-p-of-vl-interfaceinst->svex.aliases

(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: natp-of-vl-interfaceinst->svex.width

(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: natp-of-vl-interfaceinst->svex.single-width

(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: vars-of-vl-interfaceinst->svex

(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: vl-interfaceinst->svex-of-str-fix-name

(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: vl-interfaceinst->svex-streqv-congruence-on-name

(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: vl-interfaceinst->svex-of-str-fix-ifname

(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: vl-interfaceinst->svex-streqv-congruence-on-ifname

(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: vl-interfaceinst->svex-of-vl-scopestack-fix-ss

(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: vl-interfaceinst->svex-vl-scopestack-equiv-congruence-on-ss

(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: vl-interfaceinst->svex-of-maybe-natp-fix-self-lsb

(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: vl-interfaceinst->svex-maybe-nat-equiv-congruence-on-self-lsb

(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: vl-interfaceinst->svex-of-maybe-posp-fix-arraywidth

(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: vl-interfaceinst->svex-maybe-pos-equiv-congruence-on-arraywidth

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