		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-moddb.lisp

Vl-modinst->svex-assigns/aliases

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

Signature
(vl-modinst->svex-assigns/aliases x ss scopes wires assigns aliases context-mod self-lsb) → (mv vttree wires assigns1 aliases1 width modinsts modalist)
Arguments: x — Guard (vl-modinst-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).; self-lsb — Guard (maybe-natp self-lsb).
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).; width — Width if this is an interface instance.
Type (natp width).; 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-modinst->svex-assigns/aliases

(defun vl-modinst->svex-assigns/aliases
       (x ss scopes wires
          assigns aliases context-mod self-lsb)
 (declare (xargs :guard (and (vl-modinst-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)
                             (maybe-natp self-lsb))))
 (let ((__function__ 'vl-modinst->svex-assigns/aliases))
  (declare (ignorable __function__))
  (b*
   (((vl-modinst x) (vl-modinst-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)
    ((when (eq (vl-arguments-kind x.portargs)
               :vl-arguments-named))
     (mv (vfatal :type :vl-modinst->svex-fail
                 :msg "~a0: Unexpectedly had named arglist"
                 :args (list x))
         wires assigns aliases 0 nil nil))
    (x.plainargs (vl-arguments->args x.portargs))
    ((mv inst-mod inst-ss)
     (vl-scopestack-find-definition/ss x.modname ss))
    ((unless (and inst-mod
                  (or (eq (tag inst-mod) :vl-module)
                      (eq (tag inst-mod) :vl-interface))))
     (mv (vfatal :type :vl-modinst->svex-fail
                 :msg "~a0: Unknown module ~s1"
                 :args (list x x.modname))
         wires assigns aliases 0 nil nil))
    (inst-ss (vl-scopestack-push inst-mod inst-ss))
    (inst-scopes (vl-elabscopes-push-scope
                      inst-mod (vl-elabscopes-root scopes)))
    (i.ports (if (eq (tag inst-mod) :vl-module)
                 (vl-module->ports inst-mod)
               (vl-interface->ports inst-mod)))
    (inst-modname (if (eq (tag inst-mod) :vl-module)
                      (vl-module->name inst-mod)
                    (vl-interface->name inst-mod)))
    ((unless (eql (len i.ports) (len x.plainargs)))
     (mv (vfatal :type :vl-modinst->svex-fail
                 :msg "~a0: Mismatched portlist length"
                 :args (list x))
         wires assigns aliases 0 nil nil))
    ((unless (vl-maybe-range-resolved-p x.range))
     (mv (vfatal :type :vl-modinst->svex-fail
                 :msg "~a0: Unresolved instance array range"
                 :args (list x))
         wires assigns aliases 0 nil nil))
    (arraywidth (and x.range (vl-range-size x.range)))
    ((unless x.instname)
     (mv
      (vfatal
           :type :vl-modinst->svex-fail
           :msg "~a0: Unnamed module/interface instance not allowed"
           :args (list x))
      wires assigns aliases 0 nil nil))
    ((vmv vttree portinfo :ctx x)
     (vl-plainarglist-portinfo x.plainargs
                               i.ports 0 ss scopes inst-modname
                               inst-ss inst-scopes arraywidth))
    ((wvmv vttree portassigns portaliases
           :ctx x)
     (vl-portinfolist-to-svex-assigns/aliases
          portinfo x.instname x.range))
    (assigns (append-without-guard portassigns assigns))
    (aliases (append-without-guard portaliases aliases))
    ((wvmv vttree
           ifwires ifaliases arrwidth iface-width
           :ctx x)
     (if (eq (tag inst-mod) :vl-interface)
         (vl-interfaceinst->svex x.instname
                                 x.modname x ss self-lsb arraywidth)
       (mv nil nil nil 0 nil)))
    (wires (append-without-guard ifwires wires))
    (aliases (append-without-guard ifaliases aliases))
    ((unless arraywidth)
     (mv (make-vttree-context :ctx x
                              :subtree vttree)
         wires assigns aliases arrwidth
         (list (sv::make-modinst :instname x.instname
                                 :modname x.modname))
         nil))
    (array-modname (list :arraymod context-mod x.instname))
    (modinst (sv::make-modinst :instname x.instname
                               :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)
                                  inst-modname iface-width))
    (arraymod-selfwire (and (eq (tag inst-mod) :vl-interface)
                            (posp arrwidth)
                            (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)))
   (mv (make-vttree-context :ctx x
                            :subtree vttree)
       wires
       assigns aliases arrwidth (list modinst)
       (list (cons array-modname arraymod))))))

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

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

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

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

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

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

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

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

Theorem: natp-of-vl-modinst->svex-assigns/aliases.width

(defthm natp-of-vl-modinst->svex-assigns/aliases.width
  (b* (((mv ?vttree ?wires ?assigns1
            ?aliases1 ?width ?modinsts ?modalist)
        (vl-modinst->svex-assigns/aliases
             x ss scopes wires
             assigns aliases context-mod self-lsb)))
    (natp width))
  :rule-classes :type-prescription)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: vl-modinst->svex-assigns/aliases-of-maybe-natp-fix-self-lsb

(defthm vl-modinst->svex-assigns/aliases-of-maybe-natp-fix-self-lsb
  (equal (vl-modinst->svex-assigns/aliases
              x ss scopes wires assigns aliases
              context-mod (maybe-natp-fix self-lsb))
         (vl-modinst->svex-assigns/aliases
              x ss scopes wires
              assigns aliases context-mod self-lsb)))

Theorem: vl-modinst->svex-assigns/aliases-maybe-nat-equiv-congruence-on-self-lsb

(defthm
 vl-modinst->svex-assigns/aliases-maybe-nat-equiv-congruence-on-self-lsb
 (implies (acl2::maybe-nat-equiv self-lsb self-lsb-equiv)
          (equal (vl-modinst->svex-assigns/aliases
                      x ss scopes wires
                      assigns aliases context-mod self-lsb)
                 (vl-modinst->svex-assigns/aliases
                      x ss scopes wires assigns
                      aliases context-mod self-lsb-equiv)))
 :rule-classes :congruence)