• Top

• Sv::vl-moddb.lisp

Vl-instarray-nested-aliases

Signature

(vl-instarray-nested-aliases x instindex instoffset 
                             inst-incr inst-modname inst-ifacesize) 
 
  → 
(mv aliases modinsts wires)

Arguments

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

instindex — Guard (integerp instindex).

instoffset — Guard (natp instoffset).

inst-incr — Guard (integerp inst-incr).

inst-modname — Guard (sv::modname-p inst-modname).

inst-ifacesize — indicates that we're instantiating an interface, so we need :self aliases among them.
    Guard (maybe-natp inst-ifacesize).

Returns

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

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

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

Definitions and Theorems

Function: vl-instarray-nested-aliases

(defun vl-instarray-nested-aliases
       (x instindex instoffset
          inst-incr inst-modname inst-ifacesize)
 (declare (xargs :guard (and (vl-portinfolist-p x)
                             (integerp instindex)
                             (natp instoffset)
                             (integerp inst-incr)
                             (sv::modname-p inst-modname)
                             (maybe-natp inst-ifacesize))))
 (declare
      (xargs :guard (sv::svarlist-addr-p (vl-portinfolist-vars x))))
 (let ((__function__ 'vl-instarray-nested-aliases))
  (declare (ignorable __function__))
  (b*
   ((instindex (lifix instindex))
    (inst-modname (sv::modname-fix inst-modname))
    (inst-ifacesize (maybe-natp-fix inst-ifacesize))
    ((when (zp instoffset))
     (mv nil nil nil))
    (aliases2
     (and
       (posp inst-ifacesize)
       (vlsv-aggregate-aliases instindex inst-ifacesize
                               (* (1- instoffset) inst-ifacesize))))
    (wires1 (and (posp inst-ifacesize)
                 (list (sv::make-wire :name instindex
                                      :width inst-ifacesize
                                      :low-idx 0))))
    ((mv aliases3 modinsts2 wires2)
     (vl-instarray-nested-aliases
          x
          (+ (lifix instindex) (lifix inst-incr))
          (1- instoffset)
          inst-incr inst-modname inst-ifacesize)))
   (mv (append-without-guard aliases2 aliases3)
       (cons (sv::make-modinst :instname instindex
                               :modname inst-modname)
             modinsts2)
       (append-without-guard wires1 wires2)))))

Theorem: lhspairs-p-of-vl-instarray-nested-aliases.aliases

(defthm lhspairs-p-of-vl-instarray-nested-aliases.aliases
  (b* (((mv ?aliases ?modinsts ?wires)
        (vl-instarray-nested-aliases
             x instindex instoffset
             inst-incr inst-modname inst-ifacesize)))
    (sv::lhspairs-p aliases))
  :rule-classes :rewrite)

Theorem: modinstlist-p-of-vl-instarray-nested-aliases.modinsts

(defthm modinstlist-p-of-vl-instarray-nested-aliases.modinsts
  (b* (((mv ?aliases ?modinsts ?wires)
        (vl-instarray-nested-aliases
             x instindex instoffset
             inst-incr inst-modname inst-ifacesize)))
    (sv::modinstlist-p modinsts))
  :rule-classes :rewrite)

Theorem: wirelist-p-of-vl-instarray-nested-aliases.wires

(defthm wirelist-p-of-vl-instarray-nested-aliases.wires
  (b* (((mv ?aliases ?modinsts ?wires)
        (vl-instarray-nested-aliases
             x instindex instoffset
             inst-incr inst-modname inst-ifacesize)))
    (sv::wirelist-p wires))
  :rule-classes :rewrite)

Theorem: vars-of-vl-instarray-nested-instance-alias

(defthm vars-of-vl-instarray-nested-instance-alias
  (b* (((mv ?aliases ?modinsts ?wires)
        (vl-instarray-nested-aliases
             x instindex instoffset
             inst-incr inst-modname inst-ifacesize)))
    (implies (sv::svarlist-addr-p (vl-portinfolist-vars x))
             (sv::svarlist-addr-p (sv::lhspairs-vars aliases)))))

Theorem: vl-instarray-nested-aliases-of-vl-portinfolist-fix-x

(defthm vl-instarray-nested-aliases-of-vl-portinfolist-fix-x
  (equal (vl-instarray-nested-aliases
              (vl-portinfolist-fix x)
              instindex instoffset
              inst-incr inst-modname inst-ifacesize)
         (vl-instarray-nested-aliases
              x instindex instoffset
              inst-incr inst-modname inst-ifacesize)))

Theorem: vl-instarray-nested-aliases-vl-portinfolist-equiv-congruence-on-x

(defthm
  vl-instarray-nested-aliases-vl-portinfolist-equiv-congruence-on-x
  (implies (vl-portinfolist-equiv x x-equiv)
           (equal (vl-instarray-nested-aliases
                       x instindex instoffset
                       inst-incr inst-modname inst-ifacesize)
                  (vl-instarray-nested-aliases
                       x-equiv instindex instoffset
                       inst-incr inst-modname inst-ifacesize)))
  :rule-classes :congruence)

Theorem: vl-instarray-nested-aliases-of-ifix-instindex

(defthm vl-instarray-nested-aliases-of-ifix-instindex
  (equal (vl-instarray-nested-aliases
              x (ifix instindex)
              instoffset
              inst-incr inst-modname inst-ifacesize)
         (vl-instarray-nested-aliases
              x instindex instoffset
              inst-incr inst-modname inst-ifacesize)))

Theorem: vl-instarray-nested-aliases-int-equiv-congruence-on-instindex

(defthm
      vl-instarray-nested-aliases-int-equiv-congruence-on-instindex
  (implies (acl2::int-equiv instindex instindex-equiv)
           (equal (vl-instarray-nested-aliases
                       x instindex instoffset
                       inst-incr inst-modname inst-ifacesize)
                  (vl-instarray-nested-aliases
                       x instindex-equiv instoffset
                       inst-incr inst-modname inst-ifacesize)))
  :rule-classes :congruence)

Theorem: vl-instarray-nested-aliases-of-nfix-instoffset

(defthm vl-instarray-nested-aliases-of-nfix-instoffset
  (equal (vl-instarray-nested-aliases
              x instindex (nfix instoffset)
              inst-incr inst-modname inst-ifacesize)
         (vl-instarray-nested-aliases
              x instindex instoffset
              inst-incr inst-modname inst-ifacesize)))

Theorem: vl-instarray-nested-aliases-nat-equiv-congruence-on-instoffset

(defthm
     vl-instarray-nested-aliases-nat-equiv-congruence-on-instoffset
  (implies (acl2::nat-equiv instoffset instoffset-equiv)
           (equal (vl-instarray-nested-aliases
                       x instindex instoffset
                       inst-incr inst-modname inst-ifacesize)
                  (vl-instarray-nested-aliases
                       x instindex instoffset-equiv
                       inst-incr inst-modname inst-ifacesize)))
  :rule-classes :congruence)

Theorem: vl-instarray-nested-aliases-of-ifix-inst-incr

(defthm vl-instarray-nested-aliases-of-ifix-inst-incr
  (equal (vl-instarray-nested-aliases
              x instindex instoffset (ifix inst-incr)
              inst-modname inst-ifacesize)
         (vl-instarray-nested-aliases
              x instindex instoffset
              inst-incr inst-modname inst-ifacesize)))

Theorem: vl-instarray-nested-aliases-int-equiv-congruence-on-inst-incr

(defthm
      vl-instarray-nested-aliases-int-equiv-congruence-on-inst-incr
  (implies (acl2::int-equiv inst-incr inst-incr-equiv)
           (equal (vl-instarray-nested-aliases
                       x instindex instoffset
                       inst-incr inst-modname inst-ifacesize)
                  (vl-instarray-nested-aliases
                       x instindex instoffset inst-incr-equiv
                       inst-modname inst-ifacesize)))
  :rule-classes :congruence)

Theorem: vl-instarray-nested-aliases-of-modname-fix-inst-modname

(defthm vl-instarray-nested-aliases-of-modname-fix-inst-modname
  (equal (vl-instarray-nested-aliases
              x instindex instoffset
              inst-incr (sv::modname-fix inst-modname)
              inst-ifacesize)
         (vl-instarray-nested-aliases
              x instindex instoffset
              inst-incr inst-modname inst-ifacesize)))

Theorem: vl-instarray-nested-aliases-modname-equiv-congruence-on-inst-modname

(defthm
 vl-instarray-nested-aliases-modname-equiv-congruence-on-inst-modname
 (implies
  (sv::modname-equiv inst-modname inst-modname-equiv)
  (equal
   (vl-instarray-nested-aliases
        x instindex instoffset
        inst-incr inst-modname inst-ifacesize)
   (vl-instarray-nested-aliases x instindex instoffset inst-incr
                                inst-modname-equiv inst-ifacesize)))
 :rule-classes :congruence)

Theorem: vl-instarray-nested-aliases-of-maybe-natp-fix-inst-ifacesize

(defthm vl-instarray-nested-aliases-of-maybe-natp-fix-inst-ifacesize
 (equal
      (vl-instarray-nested-aliases x instindex
                                   instoffset inst-incr inst-modname
                                   (maybe-natp-fix inst-ifacesize))
      (vl-instarray-nested-aliases
           x instindex instoffset
           inst-incr inst-modname inst-ifacesize)))

Theorem: vl-instarray-nested-aliases-maybe-nat-equiv-congruence-on-inst-ifacesize

(defthm
 vl-instarray-nested-aliases-maybe-nat-equiv-congruence-on-inst-ifacesize
 (implies
  (acl2::maybe-nat-equiv inst-ifacesize inst-ifacesize-equiv)
  (equal
   (vl-instarray-nested-aliases
        x instindex instoffset
        inst-incr inst-modname inst-ifacesize)
   (vl-instarray-nested-aliases x instindex instoffset inst-incr
                                inst-modname inst-ifacesize-equiv)))
 :rule-classes :congruence)