• Top

• Sv::vl-moddb.lisp

Vl-gateinst->svex-assigns/aliases

Produces all the new svex module components associated with a VL module instance or instance array.

Signature

(vl-gateinst->svex-assigns/aliases 
     x ss scopes 
     wires assigns aliases context-mod) 
 
  → 
(mv vttree wires assigns1 aliases1 modinsts modalist)

Arguments

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

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

scopes — Guard (vl-elabscopes-p scopes).

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

assigns — Guard (sv::assigns-p assigns).

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

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

Returns

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

wires — Wires representing instantiated interfaces.
    Type (sv::wirelist-p wires).

assigns1 — Assignments for nontrivial port expressions.
    Type (sv::assigns-p assigns1).

aliases1 — Aliases for trivial port expressions.
    Type (sv::lhspairs-p aliases1).

modinsts — The instance created.
    Type (sv::modinstlist-p modinsts).

modalist — Possibly a new module implementing an instance array.
    Type (sv::modalist-p modalist).

See vl-hierarchy-sv-translation for more information on how VL module instances are translated.

Definitions and Theorems

Function: vl-gateinst->svex-assigns/aliases

(defun vl-gateinst->svex-assigns/aliases
       (x ss scopes
          wires assigns aliases context-mod)
 (declare (xargs :guard (and (vl-gateinst-p x)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes)
                             (sv::wirelist-p wires)
                             (sv::assigns-p assigns)
                             (sv::lhspairs-p aliases)
                             (sv::modname-p context-mod))))
 (let ((__function__ 'vl-gateinst->svex-assigns/aliases))
  (declare (ignorable __function__))
  (b*
   (((vl-gateinst x) (vl-gateinst-fix x))
    (wires (sv::wirelist-fix wires))
    (assigns (sv::assigns-fix assigns))
    (aliases (sv::lhspairs-fix aliases))
    (context-mod (sv::modname-fix context-mod))
    (vttree nil)
    (nargs (len x.args))
    ((mv err portnames portdirs svex-mod)
     (vl-gate-make-svex-module x.type nargs))
    ((when err)
     (mv (vfatal :type :vl-gateinst->svex-fail
                 :msg "~a0: bad gate instance: ~@1"
                 :args (list x err))
         wires assigns aliases nil nil))
    ((unless (vl-maybe-range-resolved-p x.range))
     (mv (vfatal :type :vl-gateinst->svex-fail
                 :msg "~a0: Unresolved gate instance array range"
                 :args (list x))
         wires assigns aliases nil nil))
    (arraywidth (and x.range (vl-range-size x.range)))
    ((unless x.name)
     (mv (vfatal :type :vl-gateinst->svex-fail
                 :msg "~a0: Unnamed gate instance not allowed"
                 :args (list x))
         wires assigns aliases nil nil))
    ((vmv vttree portinfo :ctx x)
     (vl-gate-plainarglist-portinfo
          x.args portnames
          portdirs 0 ss scopes arraywidth))
    ((wvmv vttree portassigns portaliases
           :ctx x)
     (vl-portinfolist-to-svex-assigns/aliases
          portinfo x.name x.range))
    (assigns (append-without-guard portassigns assigns))
    (aliases (append-without-guard portaliases aliases))
    (gate-modname
         (hons-copy (cons ':gate
                          (cons x.type (cons nargs 'nil)))))
    (modalist (list (cons gate-modname svex-mod)))
    ((unless arraywidth)
     (mv (make-vttree-context :ctx x
                              :subtree vttree)
         wires assigns aliases
         (list (sv::make-modinst :instname x.name
                                 :modname gate-modname))
         modalist))
    (array-modname (list :arraymod context-mod x.name))
    (modinst (sv::make-modinst :instname x.name
                               :modname array-modname))
    ((mv arraymod-aliases
         arraymod-modinsts arraymod-ifacewires)
     (vl-instarray-nested-aliases portinfo (vl-range-msbidx x.range)
                                  arraywidth
                                  (if (vl-range-revp x.range) 1 -1)
                                  gate-modname nil))
    (arraymod (sv::make-module :wires arraymod-ifacewires
                               :insts arraymod-modinsts
                               :aliaspairs arraymod-aliases)))
   (mv (make-vttree-context :ctx x
                            :subtree vttree)
       wires assigns aliases (list modinst)
       (cons (cons array-modname arraymod)
             modalist)))))

Theorem: return-type-of-vl-gateinst->svex-assigns/aliases.vttree

(defthm return-type-of-vl-gateinst->svex-assigns/aliases.vttree
 (b* (((mv ?vttree ?wires
           ?assigns1 ?aliases1 ?modinsts ?modalist)
       (vl-gateinst->svex-assigns/aliases
            x ss scopes
            wires assigns aliases context-mod)))
  (and
      (vttree-p vttree)
      (sv::svarlist-addr-p
           (sv::constraintlist-vars (vttree->constraints vttree)))))
 :rule-classes :rewrite)

Theorem: wirelist-p-of-vl-gateinst->svex-assigns/aliases.wires

(defthm wirelist-p-of-vl-gateinst->svex-assigns/aliases.wires
  (b* (((mv ?vttree ?wires
            ?assigns1 ?aliases1 ?modinsts ?modalist)
        (vl-gateinst->svex-assigns/aliases
             x ss scopes
             wires assigns aliases context-mod)))
    (sv::wirelist-p wires))
  :rule-classes :rewrite)

Theorem: assigns-p-of-vl-gateinst->svex-assigns/aliases.assigns1

(defthm assigns-p-of-vl-gateinst->svex-assigns/aliases.assigns1
  (b* (((mv ?vttree ?wires
            ?assigns1 ?aliases1 ?modinsts ?modalist)
        (vl-gateinst->svex-assigns/aliases
             x ss scopes
             wires assigns aliases context-mod)))
    (sv::assigns-p assigns1))
  :rule-classes :rewrite)

Theorem: lhspairs-p-of-vl-gateinst->svex-assigns/aliases.aliases1

(defthm lhspairs-p-of-vl-gateinst->svex-assigns/aliases.aliases1
  (b* (((mv ?vttree ?wires
            ?assigns1 ?aliases1 ?modinsts ?modalist)
        (vl-gateinst->svex-assigns/aliases
             x ss scopes
             wires assigns aliases context-mod)))
    (sv::lhspairs-p aliases1))
  :rule-classes :rewrite)

Theorem: modinstlist-p-of-vl-gateinst->svex-assigns/aliases.modinsts

(defthm modinstlist-p-of-vl-gateinst->svex-assigns/aliases.modinsts
  (b* (((mv ?vttree ?wires
            ?assigns1 ?aliases1 ?modinsts ?modalist)
        (vl-gateinst->svex-assigns/aliases
             x ss scopes
             wires assigns aliases context-mod)))
    (sv::modinstlist-p modinsts))
  :rule-classes :rewrite)

Theorem: modalist-p-of-vl-gateinst->svex-assigns/aliases.modalist

(defthm modalist-p-of-vl-gateinst->svex-assigns/aliases.modalist
  (b* (((mv ?vttree ?wires
            ?assigns1 ?aliases1 ?modinsts ?modalist)
        (vl-gateinst->svex-assigns/aliases
             x ss scopes
             wires assigns aliases context-mod)))
    (sv::modalist-p modalist))
  :rule-classes :rewrite)

Theorem: vars-of-vl-gateinst->svex-assigns/aliases-assigns

(defthm vars-of-vl-gateinst->svex-assigns/aliases-assigns
  (b* (((mv ?vttree ?wires
            ?assigns1 ?aliases1 ?modinsts ?modalist)
        (vl-gateinst->svex-assigns/aliases
             x ss scopes
             wires assigns aliases context-mod)))
    (implies (sv::svarlist-addr-p (sv::assigns-vars assigns))
             (sv::svarlist-addr-p (sv::assigns-vars assigns1)))))

Theorem: vars-of-vl-gateinst->svex-assigns/aliases-aliases

(defthm vars-of-vl-gateinst->svex-assigns/aliases-aliases
  (b* (((mv ?vttree ?wires
            ?assigns1 ?aliases1 ?modinsts ?modalist)
        (vl-gateinst->svex-assigns/aliases
             x ss scopes
             wires assigns aliases context-mod)))
    (implies (sv::svarlist-addr-p (sv::lhspairs-vars aliases))
             (sv::svarlist-addr-p (sv::lhspairs-vars aliases1)))))

Theorem: vars-of-vl-gateinst->svex-assigns/aliases-modalist

(defthm vars-of-vl-gateinst->svex-assigns/aliases-modalist
  (b* (((mv ?vttree ?wires
            ?assigns1 ?aliases1 ?modinsts ?modalist)
        (vl-gateinst->svex-assigns/aliases
             x ss scopes
             wires assigns aliases context-mod)))
    (sv::svarlist-addr-p (sv::modalist-vars modalist))))

Theorem: vl-gateinst->svex-assigns/aliases-of-vl-gateinst-fix-x

(defthm vl-gateinst->svex-assigns/aliases-of-vl-gateinst-fix-x
  (equal (vl-gateinst->svex-assigns/aliases
              (vl-gateinst-fix x)
              ss scopes
              wires assigns aliases context-mod)
         (vl-gateinst->svex-assigns/aliases
              x ss scopes
              wires assigns aliases context-mod)))

Theorem: vl-gateinst->svex-assigns/aliases-vl-gateinst-equiv-congruence-on-x

(defthm
 vl-gateinst->svex-assigns/aliases-vl-gateinst-equiv-congruence-on-x
 (implies (vl-gateinst-equiv x x-equiv)
          (equal (vl-gateinst->svex-assigns/aliases
                      x ss scopes
                      wires assigns aliases context-mod)
                 (vl-gateinst->svex-assigns/aliases
                      x-equiv ss scopes
                      wires assigns aliases context-mod)))
 :rule-classes :congruence)

Theorem: vl-gateinst->svex-assigns/aliases-of-vl-scopestack-fix-ss

(defthm vl-gateinst->svex-assigns/aliases-of-vl-scopestack-fix-ss
  (equal (vl-gateinst->svex-assigns/aliases
              x (vl-scopestack-fix ss)
              scopes
              wires assigns aliases context-mod)
         (vl-gateinst->svex-assigns/aliases
              x ss scopes
              wires assigns aliases context-mod)))

Theorem: vl-gateinst->svex-assigns/aliases-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-gateinst->svex-assigns/aliases-vl-scopestack-equiv-congruence-on-ss
 (implies (vl-scopestack-equiv ss ss-equiv)
          (equal (vl-gateinst->svex-assigns/aliases
                      x ss scopes
                      wires assigns aliases context-mod)
                 (vl-gateinst->svex-assigns/aliases
                      x ss-equiv scopes
                      wires assigns aliases context-mod)))
 :rule-classes :congruence)

Theorem: vl-gateinst->svex-assigns/aliases-of-vl-elabscopes-fix-scopes

(defthm
      vl-gateinst->svex-assigns/aliases-of-vl-elabscopes-fix-scopes
  (equal (vl-gateinst->svex-assigns/aliases
              x ss (vl-elabscopes-fix scopes)
              wires assigns aliases context-mod)
         (vl-gateinst->svex-assigns/aliases
              x ss scopes
              wires assigns aliases context-mod)))

Theorem: vl-gateinst->svex-assigns/aliases-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-gateinst->svex-assigns/aliases-vl-elabscopes-equiv-congruence-on-scopes
 (implies (vl-elabscopes-equiv scopes scopes-equiv)
          (equal (vl-gateinst->svex-assigns/aliases
                      x ss scopes
                      wires assigns aliases context-mod)
                 (vl-gateinst->svex-assigns/aliases
                      x ss scopes-equiv
                      wires assigns aliases context-mod)))
 :rule-classes :congruence)

Theorem: vl-gateinst->svex-assigns/aliases-of-wirelist-fix-wires

(defthm vl-gateinst->svex-assigns/aliases-of-wirelist-fix-wires
  (equal (vl-gateinst->svex-assigns/aliases
              x ss scopes (sv::wirelist-fix wires)
              assigns aliases context-mod)
         (vl-gateinst->svex-assigns/aliases
              x ss scopes
              wires assigns aliases context-mod)))

Theorem: vl-gateinst->svex-assigns/aliases-wirelist-equiv-congruence-on-wires

(defthm
 vl-gateinst->svex-assigns/aliases-wirelist-equiv-congruence-on-wires
 (implies
  (sv::wirelist-equiv wires wires-equiv)
  (equal
   (vl-gateinst->svex-assigns/aliases
        x ss scopes
        wires assigns aliases context-mod)
   (vl-gateinst->svex-assigns/aliases x ss scopes wires-equiv
                                      assigns aliases context-mod)))
 :rule-classes :congruence)

Theorem: vl-gateinst->svex-assigns/aliases-of-assigns-fix-assigns

(defthm vl-gateinst->svex-assigns/aliases-of-assigns-fix-assigns
  (equal (vl-gateinst->svex-assigns/aliases
              x ss
              scopes wires (sv::assigns-fix assigns)
              aliases context-mod)
         (vl-gateinst->svex-assigns/aliases
              x ss scopes
              wires assigns aliases context-mod)))

Theorem: vl-gateinst->svex-assigns/aliases-assigns-equiv-congruence-on-assigns

(defthm
 vl-gateinst->svex-assigns/aliases-assigns-equiv-congruence-on-assigns
 (implies (sv::assigns-equiv assigns assigns-equiv)
          (equal (vl-gateinst->svex-assigns/aliases
                      x ss scopes
                      wires assigns aliases context-mod)
                 (vl-gateinst->svex-assigns/aliases
                      x ss scopes wires
                      assigns-equiv aliases context-mod)))
 :rule-classes :congruence)

Theorem: vl-gateinst->svex-assigns/aliases-of-lhspairs-fix-aliases

(defthm vl-gateinst->svex-assigns/aliases-of-lhspairs-fix-aliases
  (equal (vl-gateinst->svex-assigns/aliases
              x ss scopes
              wires assigns (sv::lhspairs-fix aliases)
              context-mod)
         (vl-gateinst->svex-assigns/aliases
              x ss scopes
              wires assigns aliases context-mod)))

Theorem: vl-gateinst->svex-assigns/aliases-lhspairs-equiv-congruence-on-aliases

(defthm
 vl-gateinst->svex-assigns/aliases-lhspairs-equiv-congruence-on-aliases
 (implies (sv::lhspairs-equiv aliases aliases-equiv)
          (equal (vl-gateinst->svex-assigns/aliases
                      x ss scopes
                      wires assigns aliases context-mod)
                 (vl-gateinst->svex-assigns/aliases
                      x ss scopes wires
                      assigns aliases-equiv context-mod)))
 :rule-classes :congruence)

Theorem: vl-gateinst->svex-assigns/aliases-of-modname-fix-context-mod

(defthm vl-gateinst->svex-assigns/aliases-of-modname-fix-context-mod
  (equal (vl-gateinst->svex-assigns/aliases
              x ss scopes wires assigns
              aliases (sv::modname-fix context-mod))
         (vl-gateinst->svex-assigns/aliases
              x ss scopes
              wires assigns aliases context-mod)))

Theorem: vl-gateinst->svex-assigns/aliases-modname-equiv-congruence-on-context-mod

(defthm
 vl-gateinst->svex-assigns/aliases-modname-equiv-congruence-on-context-mod
 (implies (sv::modname-equiv context-mod context-mod-equiv)
          (equal (vl-gateinst->svex-assigns/aliases
                      x ss scopes
                      wires assigns aliases context-mod)
                 (vl-gateinst->svex-assigns/aliases
                      x ss scopes wires
                      assigns aliases context-mod-equiv)))
 :rule-classes :congruence)