• Top

• Sv::vl-moddb.lisp

Vl-interfaceport->svex

Produces svex wires, insts, aliases for an interface port.

Signature

(vl-interfaceport->svex x ss self-lsb context-mod) 
  → 
(mv warnings wires insts aliases modalist width)

Arguments

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

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

self-lsb — Guard (maybe-natp self-lsb).

context-mod — Guard (sv::modname-p context-mod).

Returns

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

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

insts — Type (sv::modinstlist-p insts).

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

modalist — Type (sv::modalist-p modalist).

width — Type (natp width).

Just adds a modinst to the outputs of vl-interfaceinst->svex.

Definitions and Theorems

Function: vl-interfaceport->svex

(defun vl-interfaceport->svex (x ss self-lsb context-mod)
 (declare (xargs :guard (and (vl-interfaceport-p x)
                             (vl-scopestack-p ss)
                             (maybe-natp self-lsb)
                             (sv::modname-p context-mod))))
 (let ((__function__ 'vl-interfaceport->svex))
  (declare (ignorable __function__))
  (b*
   (((vl-interfaceport x)
     (vl-interfaceport-fix x))
    (context-mod (sv::modname-fix context-mod))
    (warnings nil)
    ((unless
      (or
       (atom x.udims)
       (and
        (atom (cdr x.udims))
        (vl-dimension-case (car x.udims) :range)
        (vl-range-resolved-p (vl-dimension->range (car x.udims))))))
     (mv
      (fatal
       :type :vl-bad-interfaceport-array
       :msg
       "Unresolved or unsized dimensions on interfaceport array: ~a0"
       :args (list x))
      nil nil nil nil 0))
    (range (and (consp x.udims)
                (vl-dimension->range (car x.udims))))
    (arraysize (and range (vl-range-size range)))
    ((wmv warnings
          wires aliases arrwidth singlewidth)
     (vl-interfaceinst->svex x.name
                             x.ifname x ss self-lsb arraysize))
    ((unless (and arraysize (posp arrwidth)))
     (mv warnings wires
         (list (sv::make-modinst :instname x.name
                                 :modname x.ifname))
         aliases nil arrwidth))
    ((mv arraymod-aliases
         arraymod-modinsts arraymod-ifacewires)
     (vl-instarray-nested-aliases
          nil
          (vl-resolved->val (vl-range->msb range))
          arraysize
          (if (vl-range-revp range) 1 -1)
          x.ifname singlewidth))
    (arraymod-selfwire (list (sv::make-wire :name :self
                                            :width arrwidth
                                            :low-idx 0)))
    (arraymod
         (sv::make-module
              :wires (append arraymod-selfwire arraymod-ifacewires)
              :insts arraymod-modinsts
              :aliaspairs arraymod-aliases))
    (array-modname (list :array-ifportmod context-mod x.name))
    (insts (list (sv::make-modinst :instname x.name
                                   :modname array-modname))))
   (mv warnings wires insts aliases
       (list (cons array-modname arraymod))
       arrwidth))))

Theorem: vl-warninglist-p-of-vl-interfaceport->svex.warnings

(defthm vl-warninglist-p-of-vl-interfaceport->svex.warnings
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceport->svex x ss self-lsb context-mod)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: wirelist-p-of-vl-interfaceport->svex.wires

(defthm wirelist-p-of-vl-interfaceport->svex.wires
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceport->svex x ss self-lsb context-mod)))
    (sv::wirelist-p wires))
  :rule-classes :rewrite)

Theorem: modinstlist-p-of-vl-interfaceport->svex.insts

(defthm modinstlist-p-of-vl-interfaceport->svex.insts
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceport->svex x ss self-lsb context-mod)))
    (sv::modinstlist-p insts))
  :rule-classes :rewrite)

Theorem: lhspairs-p-of-vl-interfaceport->svex.aliases

(defthm lhspairs-p-of-vl-interfaceport->svex.aliases
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceport->svex x ss self-lsb context-mod)))
    (sv::lhspairs-p aliases))
  :rule-classes :rewrite)

Theorem: modalist-p-of-vl-interfaceport->svex.modalist

(defthm modalist-p-of-vl-interfaceport->svex.modalist
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceport->svex x ss self-lsb context-mod)))
    (sv::modalist-p modalist))
  :rule-classes :rewrite)

Theorem: natp-of-vl-interfaceport->svex.width

(defthm natp-of-vl-interfaceport->svex.width
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceport->svex x ss self-lsb context-mod)))
    (natp width))
  :rule-classes :type-prescription)

Theorem: vars-of-vl-interfaceport->svex

(defthm vars-of-vl-interfaceport->svex
  (b* (((mv ?warnings
            ?wires ?insts ?aliases ?modalist ?width)
        (vl-interfaceport->svex x ss self-lsb context-mod)))
    (and (sv::svarlist-addr-p (sv::lhspairs-vars aliases))
         (sv::svarlist-addr-p (sv::modalist-vars modalist)))))

Theorem: vl-interfaceport->svex-of-vl-interfaceport-fix-x

(defthm vl-interfaceport->svex-of-vl-interfaceport-fix-x
  (equal (vl-interfaceport->svex (vl-interfaceport-fix x)
                                 ss self-lsb context-mod)
         (vl-interfaceport->svex x ss self-lsb context-mod)))

Theorem: vl-interfaceport->svex-vl-interfaceport-equiv-congruence-on-x

(defthm
      vl-interfaceport->svex-vl-interfaceport-equiv-congruence-on-x
 (implies
   (vl-interfaceport-equiv x x-equiv)
   (equal (vl-interfaceport->svex x ss self-lsb context-mod)
          (vl-interfaceport->svex x-equiv ss self-lsb context-mod)))
 :rule-classes :congruence)

Theorem: vl-interfaceport->svex-of-vl-scopestack-fix-ss

(defthm vl-interfaceport->svex-of-vl-scopestack-fix-ss
  (equal (vl-interfaceport->svex x (vl-scopestack-fix ss)
                                 self-lsb context-mod)
         (vl-interfaceport->svex x ss self-lsb context-mod)))

Theorem: vl-interfaceport->svex-vl-scopestack-equiv-congruence-on-ss

(defthm vl-interfaceport->svex-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal (vl-interfaceport->svex x ss self-lsb context-mod)
          (vl-interfaceport->svex x ss-equiv self-lsb context-mod)))
 :rule-classes :congruence)

Theorem: vl-interfaceport->svex-of-maybe-natp-fix-self-lsb

(defthm vl-interfaceport->svex-of-maybe-natp-fix-self-lsb
  (equal (vl-interfaceport->svex x ss (maybe-natp-fix self-lsb)
                                 context-mod)
         (vl-interfaceport->svex x ss self-lsb context-mod)))

Theorem: vl-interfaceport->svex-maybe-nat-equiv-congruence-on-self-lsb

(defthm
      vl-interfaceport->svex-maybe-nat-equiv-congruence-on-self-lsb
 (implies
   (acl2::maybe-nat-equiv self-lsb self-lsb-equiv)
   (equal (vl-interfaceport->svex x ss self-lsb context-mod)
          (vl-interfaceport->svex x ss self-lsb-equiv context-mod)))
 :rule-classes :congruence)

Theorem: vl-interfaceport->svex-of-modname-fix-context-mod

(defthm vl-interfaceport->svex-of-modname-fix-context-mod
 (equal
     (vl-interfaceport->svex x ss
                             self-lsb (sv::modname-fix context-mod))
     (vl-interfaceport->svex x ss self-lsb context-mod)))

Theorem: vl-interfaceport->svex-modname-equiv-congruence-on-context-mod

(defthm
     vl-interfaceport->svex-modname-equiv-congruence-on-context-mod
 (implies
   (sv::modname-equiv context-mod context-mod-equiv)
   (equal (vl-interfaceport->svex x ss self-lsb context-mod)
          (vl-interfaceport->svex x ss self-lsb context-mod-equiv)))
 :rule-classes :congruence)