• Top

• Sv::vl-moddb.lisp

Vl-vardecllist->svex

Collects svex module components for a list of vardecls, by collecting results from vl-vardecl->svex.

Signature

(vl-vardecllist->svex x portdecls 
                      modalist interfacep ss scopes config) 
 
  → 
(mv vttree width wires fixups aliases modinsts assigns modalist1)

Arguments

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

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

interfacep — controls whether we create aliases between the local :self wire and the vars, as we must for the vardecls within an interface.

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

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

config — Guard (vl-simpconfig-p config).

Returns

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

width — Type (natp width).

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

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

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

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

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

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

Definitions and Theorems

Function: vl-vardecllist->svex

(defun vl-vardecllist->svex (x portdecls
                               modalist interfacep ss scopes config)
 (declare (xargs :guard (and (vl-vardecllist-p x)
                             (sv::modalist-p modalist)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-vardecllist->svex))
  (declare (ignorable __function__))
  (b* (((when (atom x))
        (mv nil 0 nil nil nil
            nil nil (sv::modalist-fix modalist)))
       (vttree nil)
       ((vmv vttree width2 wires2 fixups2
             aliases2 modinsts2 assigns2 modalist)
        (vl-vardecllist->svex (cdr x)
                              portdecls
                              modalist interfacep ss scopes config))
       ((vmv vttree width1 wire1 fixups1
             aliases1 modinsts1 assigns1 modalist)
        (vl-vardecl->svex (car x)
                          portdecls
                          modalist (and interfacep width2)
                          ss scopes config)))
    (mv vttree (+ width1 width2)
        (append-without-guard wire1 wires2)
        (append-without-guard fixups1 fixups2)
        (append-without-guard aliases1 aliases2)
        (append-without-guard modinsts1 modinsts2)
        (append-without-guard assigns1 assigns2)
        modalist))))

Theorem: return-type-of-vl-vardecllist->svex.vttree

(defthm return-type-of-vl-vardecllist->svex.vttree
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
  (and
      (vttree-p vttree)
      (sv::svarlist-addr-p
           (sv::constraintlist-vars (vttree->constraints vttree)))))
 :rule-classes :rewrite)

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

(defthm natp-of-vl-vardecllist->svex.width
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (natp width))
 :rule-classes :type-prescription)

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

(defthm wirelist-p-of-vl-vardecllist->svex.wires
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::wirelist-p wires))
 :rule-classes :rewrite)

Theorem: assigns-p-of-vl-vardecllist->svex.fixups

(defthm assigns-p-of-vl-vardecllist->svex.fixups
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::assigns-p fixups))
 :rule-classes :rewrite)

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

(defthm lhspairs-p-of-vl-vardecllist->svex.aliases
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::lhspairs-p aliases))
 :rule-classes :rewrite)

Theorem: modinstlist-p-of-vl-vardecllist->svex.modinsts

(defthm modinstlist-p-of-vl-vardecllist->svex.modinsts
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::modinstlist-p modinsts))
 :rule-classes :rewrite)

Theorem: assigns-p-of-vl-vardecllist->svex.assigns

(defthm assigns-p-of-vl-vardecllist->svex.assigns
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::assigns-p assigns))
 :rule-classes :rewrite)

Theorem: modalist-p-of-vl-vardecllist->svex.modalist1

(defthm modalist-p-of-vl-vardecllist->svex.modalist1
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::modalist-p modalist1))
 :rule-classes :rewrite)

Theorem: vars-of-vl-vardecllist->svex-modalist

(defthm vars-of-vl-vardecllist->svex-modalist
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (implies (sv::svarlist-addr-p (sv::modalist-vars modalist))
            (sv::svarlist-addr-p (sv::modalist-vars modalist1)))))

Theorem: vars-of-vl-vardecllist->svex-aliases

(defthm vars-of-vl-vardecllist->svex-aliases
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))

Theorem: vars-of-vl-vardecllist->svex-fixups

(defthm vars-of-vl-vardecllist->svex-fixups
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::svarlist-addr-p (sv::assigns-vars fixups))))

Theorem: vars-of-vl-vardecllist->svex-assigns

(defthm vars-of-vl-vardecllist->svex-assigns
 (b* (((mv ?vttree ?width ?wires ?fixups
           ?aliases ?modinsts ?assigns ?modalist1)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))
   (sv::svarlist-addr-p (sv::assigns-vars assigns))))

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

(defthm vl-vardecllist->svex-of-vl-vardecllist-fix-x
  (equal
       (vl-vardecllist->svex (vl-vardecllist-fix x)
                             portdecls
                             modalist interfacep ss scopes config)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))

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

(defthm vl-vardecllist->svex-vl-vardecllist-equiv-congruence-on-x
 (implies
  (vl-vardecllist-equiv x x-equiv)
  (equal
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)
       (vl-vardecllist->svex x-equiv portdecls
                             modalist interfacep ss scopes config)))
 :rule-classes :congruence)

Theorem: vl-vardecllist->svex-of-modalist-fix-modalist

(defthm vl-vardecllist->svex-of-modalist-fix-modalist
  (equal
       (vl-vardecllist->svex x portdecls (sv::modalist-fix modalist)
                             interfacep ss scopes config)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))

Theorem: vl-vardecllist->svex-modalist-equiv-congruence-on-modalist

(defthm vl-vardecllist->svex-modalist-equiv-congruence-on-modalist
 (implies
  (sv::modalist-equiv modalist modalist-equiv)
  (equal (vl-vardecllist->svex x portdecls
                               modalist interfacep ss scopes config)
         (vl-vardecllist->svex x portdecls modalist-equiv
                               interfacep ss scopes config)))
 :rule-classes :congruence)

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

(defthm vl-vardecllist->svex-of-vl-scopestack-fix-ss
  (equal
       (vl-vardecllist->svex x portdecls modalist
                             interfacep (vl-scopestack-fix ss)
                             scopes config)
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))

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

(defthm vl-vardecllist->svex-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-vardecllist->svex x portdecls
                               modalist interfacep ss scopes config)
         (vl-vardecllist->svex x portdecls modalist
                               interfacep ss-equiv scopes config)))
 :rule-classes :congruence)

Theorem: vl-vardecllist->svex-of-vl-elabscopes-fix-scopes

(defthm vl-vardecllist->svex-of-vl-elabscopes-fix-scopes
 (equal
      (vl-vardecllist->svex x portdecls modalist
                            interfacep ss (vl-elabscopes-fix scopes)
                            config)
      (vl-vardecllist->svex x portdecls
                            modalist interfacep ss scopes config)))

Theorem: vl-vardecllist->svex-vl-elabscopes-equiv-congruence-on-scopes

(defthm
      vl-vardecllist->svex-vl-elabscopes-equiv-congruence-on-scopes
 (implies
  (vl-elabscopes-equiv scopes scopes-equiv)
  (equal (vl-vardecllist->svex x portdecls
                               modalist interfacep ss scopes config)
         (vl-vardecllist->svex x portdecls modalist
                               interfacep ss scopes-equiv config)))
 :rule-classes :congruence)

Theorem: vl-vardecllist->svex-of-vl-simpconfig-fix-config

(defthm vl-vardecllist->svex-of-vl-simpconfig-fix-config
  (equal
       (vl-vardecllist->svex x portdecls modalist interfacep
                             ss scopes (vl-simpconfig-fix config))
       (vl-vardecllist->svex x portdecls
                             modalist interfacep ss scopes config)))

Theorem: vl-vardecllist->svex-vl-simpconfig-equiv-congruence-on-config

(defthm
      vl-vardecllist->svex-vl-simpconfig-equiv-congruence-on-config
 (implies
  (vl-simpconfig-equiv config config-equiv)
  (equal (vl-vardecllist->svex x portdecls
                               modalist interfacep ss scopes config)
         (vl-vardecllist->svex x portdecls modalist
                               interfacep ss scopes config-equiv)))
 :rule-classes :congruence)