Iterates over the indices of an array, creating svex module components for each index using vl-datatype-elem->mod-components
(vl-datatype-dimension->mod-components count msi incr subwire submod) → (mv wires insts aliases)
Function:
(defun vl-datatype-dimension->mod-components (count msi incr subwire submod) (declare (xargs :guard (and (natp count) (integerp msi) (integerp incr) (sv::wire-p subwire) (or (sv::modname-p submod) (not submod))))) (let ((__function__ 'vl-datatype-dimension->mod-components)) (declare (ignorable __function__)) (mbe :logic (b* (((when (zp count)) (mv nil nil nil)) (next-count (1- count)) ((mv wire1 insts1 aliases1) (vl-datatype-elem->mod-components (lifix msi) subwire (* (sv::wire->width subwire) next-count) submod)) ((mv wires insts aliases) (vl-datatype-dimension->mod-components next-count (+ (lifix incr) (lifix msi)) incr subwire submod))) (mv (cons wire1 wires) (append-without-guard insts1 insts) (append-without-guard aliases1 aliases))) :exec (vl-datatype-dimension->mod-components-tr count msi incr subwire submod nil nil nil))))
Theorem:
(defthm wirelist-p-of-vl-datatype-dimension->mod-components.wires (b* (((mv ?wires ?insts ?aliases) (vl-datatype-dimension->mod-components count msi incr subwire submod))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-datatype-dimension->mod-components.insts (b* (((mv ?wires ?insts ?aliases) (vl-datatype-dimension->mod-components count msi incr subwire submod))) (sv::modinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-datatype-dimension->mod-components.aliases (b* (((mv ?wires ?insts ?aliases) (vl-datatype-dimension->mod-components count msi incr subwire submod))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-datatype-dimension->mod-components (b* (((mv ?wires ?insts ?aliases) (vl-datatype-dimension->mod-components count msi incr subwire submod))) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-dimension->mod-components-of-nfix-count (equal (vl-datatype-dimension->mod-components (nfix count) msi incr subwire submod) (vl-datatype-dimension->mod-components count msi incr subwire submod)))
Theorem:
(defthm vl-datatype-dimension->mod-components-nat-equiv-congruence-on-count (implies (acl2::nat-equiv count count-equiv) (equal (vl-datatype-dimension->mod-components count msi incr subwire submod) (vl-datatype-dimension->mod-components count-equiv msi incr subwire submod))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-of-ifix-msi (equal (vl-datatype-dimension->mod-components count (ifix msi) incr subwire submod) (vl-datatype-dimension->mod-components count msi incr subwire submod)))
Theorem:
(defthm vl-datatype-dimension->mod-components-int-equiv-congruence-on-msi (implies (acl2::int-equiv msi msi-equiv) (equal (vl-datatype-dimension->mod-components count msi incr subwire submod) (vl-datatype-dimension->mod-components count msi-equiv incr subwire submod))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-of-ifix-incr (equal (vl-datatype-dimension->mod-components count msi (ifix incr) subwire submod) (vl-datatype-dimension->mod-components count msi incr subwire submod)))
Theorem:
(defthm vl-datatype-dimension->mod-components-int-equiv-congruence-on-incr (implies (acl2::int-equiv incr incr-equiv) (equal (vl-datatype-dimension->mod-components count msi incr subwire submod) (vl-datatype-dimension->mod-components count msi incr-equiv subwire submod))) :rule-classes :congruence)
Theorem:
(defthm vl-datatype-dimension->mod-components-of-wire-fix-subwire (equal (vl-datatype-dimension->mod-components count msi incr (sv::wire-fix subwire) submod) (vl-datatype-dimension->mod-components count msi incr subwire submod)))
Theorem:
(defthm vl-datatype-dimension->mod-components-wire-equiv-congruence-on-subwire (implies (sv::wire-equiv subwire subwire-equiv) (equal (vl-datatype-dimension->mod-components count msi incr subwire submod) (vl-datatype-dimension->mod-components count msi incr subwire-equiv submod))) :rule-classes :congruence)