(vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr) → assigns
Function:
(defun vl-instarray-replicated-port-assigns (port-lhs instname conn-driver instindex instoffset inst-incr) (declare (xargs :guard (and (sv::lhs-p port-lhs) (stringp instname) (sv::driver-p conn-driver) (integerp instindex) (natp instoffset) (integerp inst-incr)))) (declare (xargs :guard (and (sv::svarlist-addr-p (sv::lhs-vars port-lhs)) (sv::svarlist-addr-p (sv::svex-vars (sv::driver->value conn-driver)))))) (let ((__function__ 'vl-instarray-replicated-port-assigns)) (declare (ignorable __function__)) (b* (((when (zp instoffset)) nil) (instindex (lifix instindex)) (lhs1 (sv::lhs-add-namespace (string-fix instname) (sv::lhs-add-namespace instindex port-lhs)))) (cons (cons lhs1 (sv::driver-fix conn-driver)) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver (+ instindex (lifix inst-incr)) (1- instoffset) inst-incr)))))
Theorem:
(defthm assigns-p-of-vl-instarray-replicated-port-assigns (b* ((assigns (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr))) (sv::assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-vl-instarray-replicated-port-assigns (b* ((?assigns (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr))) (implies (sv::svarlist-addr-p (sv::svex-vars (sv::driver->value conn-driver))) (sv::svarlist-addr-p (sv::assigns-vars assigns)))))
Theorem:
(defthm vl-instarray-replicated-port-assigns-of-lhs-fix-port-lhs (equal (vl-instarray-replicated-port-assigns (sv::lhs-fix port-lhs) instname conn-driver instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-assigns-lhs-equiv-congruence-on-port-lhs (implies (sv::lhs-equiv port-lhs port-lhs-equiv) (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs-equiv instname conn-driver instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-assigns-of-str-fix-instname (equal (vl-instarray-replicated-port-assigns port-lhs (str-fix instname) conn-driver instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-assigns-streqv-congruence-on-instname (implies (streqv instname instname-equiv) (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname-equiv conn-driver instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-assigns-of-driver-fix-conn-driver (equal (vl-instarray-replicated-port-assigns port-lhs instname (sv::driver-fix conn-driver) instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-assigns-driver-equiv-congruence-on-conn-driver (implies (sv::driver-equiv conn-driver conn-driver-equiv) (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver-equiv instindex instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-assigns-of-ifix-instindex (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver (ifix instindex) instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-assigns-int-equiv-congruence-on-instindex (implies (acl2::int-equiv instindex instindex-equiv) (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex-equiv instoffset inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-assigns-of-nfix-instoffset (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex (nfix instoffset) inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-assigns-nat-equiv-congruence-on-instoffset (implies (acl2::nat-equiv instoffset instoffset-equiv) (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset-equiv inst-incr))) :rule-classes :congruence)
Theorem:
(defthm vl-instarray-replicated-port-assigns-of-ifix-inst-incr (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset (ifix inst-incr)) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr)))
Theorem:
(defthm vl-instarray-replicated-port-assigns-int-equiv-congruence-on-inst-incr (implies (acl2::int-equiv inst-incr inst-incr-equiv) (equal (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr) (vl-instarray-replicated-port-assigns port-lhs instname conn-driver instindex instoffset inst-incr-equiv))) :rule-classes :congruence)