(vl-emodwires-from-high-to-low name high low) returns a list of vl-emodwire-ps:
The range is inclusive on both sides, so if
Function:
(defun vl-emodwires-from-high-to-low-aux (name high low acc) (declare (type string name) (xargs :guard (and (natp high) (natp low) (>= high low)))) (b* ((name[low] (vl-emodwire-encoded name low)) (acc (cons name[low] acc)) ((when (mbe :logic (<= (nfix high) (nfix low)) :exec (= high low))) acc)) (vl-emodwires-from-high-to-low-aux name (lnfix high) (+ 1 (lnfix low)) acc)))
Function:
(defun vl-emodwires-from-high-to-low-aux-fixnum$inline (name high low acc) (declare (type string name) (type (unsigned-byte 32) high) (type (unsigned-byte 32) low) (xargs :guard (>= high low))) (b* ((name[low] (mbe :logic (vl-emodwire-encoded name low) :exec (if (< (the (unsigned-byte 32) low) 256) (intern (cat name (aref1 '*vl-indexed-wire-name-array* *vl-indexed-wire-name-array* low)) "ACL2") (intern (cat name "[" (natstr low) "]") "ACL2")))) (acc (cons name[low] acc)) ((when (mbe :logic (<= (nfix high) (nfix low)) :exec (= (the (unsigned-byte 32) high) (the (unsigned-byte 32) low)))) acc)) (vl-emodwires-from-high-to-low-aux-fixnum name (lnfix high) (mbe :logic (+ 1 (nfix low)) :exec (the (unsigned-byte 32) (+ low 1))) acc)))
Function:
(defun vl-emodwires-from-high-to-low (name high low) (declare (type string name) (xargs :guard (and (natp high) (natp low) (>= high low)))) (mbe :logic (vl-emodwires-from-high-to-low-aux (vl-emodwire-encode (string-fix name)) (nfix high) (nfix low) nil) :exec (let ((name (vl-emodwire-encode name))) (if (< high (expt 2 30)) (vl-emodwires-from-high-to-low-aux-fixnum name high low nil) (vl-emodwires-from-high-to-low-aux name high low nil)))))
Theorem:
(defthm true-listp-of-vl-emodwires-from-high-to-low (true-listp (vl-emodwires-from-high-to-low name high low)) :rule-classes :type-prescription)
Theorem:
(defthm vl-emodwirelist-p-of-vl-emodwires-from-high-to-low (vl-emodwirelist-p (vl-emodwires-from-high-to-low name high low)))
Theorem:
(defthm basenames-of-vl-emodwires-from-high-to-low (equal (vl-emodwirelist->basenames (vl-emodwires-from-high-to-low name high low)) (replicate (len (vl-emodwires-from-high-to-low name high low)) (string-fix name))))
Theorem:
(defthm member-equal-of-indicies-of-vl-emodwires-from-high-to-low (implies (>= (nfix high) (nfix low)) (iff (member-equal idx (vl-emodwirelist->indices (vl-emodwires-from-high-to-low name high low))) (and (natp idx) (<= (nfix low) idx) (<= idx (nfix high))))))
Theorem:
(defthm unique-indicies-of-vl-emodwires-from-high-to-low (no-duplicatesp-equal (vl-emodwirelist->indices (vl-emodwires-from-high-to-low name high low))))
Theorem:
(defthm no-duplicatesp-equal-of-vl-emodwires-from-high-to-low (no-duplicatesp-equal (vl-emodwires-from-high-to-low name high low)))
Theorem:
(defthm len-of-vl-emodwires-from-high-to-low (equal (len (vl-emodwires-from-high-to-low name high low)) (+ 1 (nfix (- (nfix high) (nfix low))))))