(vl-instarray-nested-aliases x instindex instoffset inst-incr inst-modname inst-ifacesize) → (mv aliases modinsts wires)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)