Generate the Verilog-style names of the original instances (e.g., names with square-bracketed indices).
(vl-replicate-orig-instnames instname instrange) → names
These names are just going to be attributes for the new instances, which allow you to relate the original Verilog with the simplified Verilog. The order must match vl-replicated-instnames.
Function:
(defun vl-replicate-orig-instnames (instname instrange) (declare (xargs :guard (and (maybe-stringp instname) (vl-range-p instrange)))) (declare (xargs :guard (vl-range-resolved-p instrange))) (let ((__function__ 'vl-replicate-orig-instnames)) (declare (ignorable __function__)) (b* ((left (vl-resolved->val (vl-range->msb instrange))) (right (vl-resolved->val (vl-range->lsb instrange))) (low (min left right)) (high (max left right)) (instname (or instname "unnamed")) (low-to-high (vl-replicate-orig-instnames1 low high instname))) (if (>= left right) (reverse low-to-high) low-to-high))))
Theorem:
(defthm string-listp-of-vl-replicate-orig-instnames (b* ((names (vl-replicate-orig-instnames instname instrange))) (string-listp names)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-replicate-orig-instnames (equal (len (vl-replicate-orig-instnames instname instrange)) (vl-range-size instrange)))
Theorem:
(defthm vl-replicate-orig-instnames-of-maybe-string-fix-instname (equal (vl-replicate-orig-instnames (maybe-string-fix instname) instrange) (vl-replicate-orig-instnames instname instrange)))
Theorem:
(defthm vl-replicate-orig-instnames-maybe-string-equiv-congruence-on-instname (implies (maybe-string-equiv instname instname-equiv) (equal (vl-replicate-orig-instnames instname instrange) (vl-replicate-orig-instnames instname-equiv instrange))) :rule-classes :congruence)
Theorem:
(defthm vl-replicate-orig-instnames-of-vl-range-fix-instrange (equal (vl-replicate-orig-instnames instname (vl-range-fix instrange)) (vl-replicate-orig-instnames instname instrange)))
Theorem:
(defthm vl-replicate-orig-instnames-vl-range-equiv-congruence-on-instrange (implies (vl-range-equiv instrange instrange-equiv) (equal (vl-replicate-orig-instnames instname instrange) (vl-replicate-orig-instnames instname instrange-equiv))) :rule-classes :congruence)