• Top

• Sv::vl-moddb.lisp

Vl-modinstlist->svex-assigns/aliases

Collects svex module components for a list of module/interface instances, by collecting results from vl-modinst->svex-assigns/aliases.

Signature

(vl-modinstlist->svex-assigns/aliases 
     x ss scopes wires 
     assigns aliases context-mod self-lsb) 
 
  → 
(mv vttree wires1 assigns1 aliases1 width modinsts modalist)

Arguments

x — Guard (vl-modinstlist-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)))) .

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

assigns1 — Type (sv::assigns-p assigns1).

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

width — Type (natp width).

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

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

Definitions and Theorems

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

(defun vl-modinstlist->svex-assigns/aliases
       (x ss scopes wires
          assigns aliases context-mod self-lsb)
  (declare (xargs :guard (and (vl-modinstlist-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-modinstlist->svex-assigns/aliases))
    (declare (ignorable __function__))
    (b* ((vttree nil)
         ((when (atom x))
          (mv nil (sv::wirelist-fix wires)
              (sv::assigns-fix assigns)
              (sv::lhspairs-fix aliases)
              0 nil nil))
         (self-lsb (maybe-natp-fix self-lsb))
         ((vmv vttree wires
               assigns aliases width2 insts2 modalist2)
          (vl-modinstlist->svex-assigns/aliases
               (cdr x)
               ss scopes wires
               assigns aliases context-mod self-lsb))
         ((vmv vttree wires
               assigns aliases width1 insts1 modalist1)
          (vl-modinst->svex-assigns/aliases
               (car x)
               ss
               scopes wires assigns aliases context-mod
               (and self-lsb (+ self-lsb width2)))))
      (mv vttree
          wires assigns aliases (+ width1 width2)
          (append-without-guard insts1 insts2)
          (append-without-guard modalist1 modalist2)))))

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

(defthm return-type-of-vl-modinstlist->svex-assigns/aliases.vttree
 (b* (((mv ?vttree ?wires1 ?assigns1
           ?aliases1 ?width ?modinsts ?modalist)
       (vl-modinstlist->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-modinstlist->svex-assigns/aliases.wires1

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

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

(defthm assigns-p-of-vl-modinstlist->svex-assigns/aliases.assigns1
  (b* (((mv ?vttree ?wires1 ?assigns1
            ?aliases1 ?width ?modinsts ?modalist)
        (vl-modinstlist->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-modinstlist->svex-assigns/aliases.aliases1

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

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

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

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

(defthm
     modinstlist-p-of-vl-modinstlist->svex-assigns/aliases.modinsts
  (b* (((mv ?vttree ?wires1 ?assigns1
            ?aliases1 ?width ?modinsts ?modalist)
        (vl-modinstlist->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-modinstlist->svex-assigns/aliases.modalist

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

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

(defthm vars-of-vl-modinstlist->svex-assigns/aliases-assigns
  (b* (((mv ?vttree ?wires1 ?assigns1
            ?aliases1 ?width ?modinsts ?modalist)
        (vl-modinstlist->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-modinstlist->svex-assigns/aliases-aliases

(defthm vars-of-vl-modinstlist->svex-assigns/aliases-aliases
  (b* (((mv ?vttree ?wires1 ?assigns1
            ?aliases1 ?width ?modinsts ?modalist)
        (vl-modinstlist->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-modinstlist->svex-assigns/aliases-modalist

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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