Build a list of expressions,
(vl-make-list-of-bitselects expr low high) → exprs
Function:
(defun vl-make-list-of-bitselects (expr low high) (declare (xargs :guard (and (vl-expr-p expr) (natp low) (natp high)))) (declare (xargs :guard (<= low high))) (let ((__function__ 'vl-make-list-of-bitselects)) (declare (ignorable __function__)) (if (mbe :logic (zp (- (nfix high) (nfix low))) :exec (eql high low)) (list (vl-make-bitselect expr low)) (cons (vl-make-bitselect expr low) (vl-make-list-of-bitselects expr (+ (nfix low) 1) high)))))
Theorem:
(defthm vl-exprlist-p-of-vl-make-list-of-bitselects (b* ((exprs (vl-make-list-of-bitselects expr low high))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-make-list-of-bitselects (equal (len (vl-make-list-of-bitselects expr low high)) (+ 1 (nfix (- (nfix high) (nfix low))))))
Theorem:
(defthm vl-exprlist->finalwidths-of-vl-make-list-of-bitselects (equal (vl-exprlist->finalwidths (vl-make-list-of-bitselects expr low high)) (replicate (+ 1 (nfix (- (nfix high) (nfix low)))) 1)))
Theorem:
(defthm vl-exprlist->finaltypes-of-vl-make-list-of-bitselects (equal (vl-exprlist->finaltypes (vl-make-list-of-bitselects expr low high)) (replicate (+ 1 (nfix (- (nfix high) (nfix low)))) :vl-unsigned)))
Theorem:
(defthm vl-make-list-of-bitselects-of-vl-expr-fix-expr (equal (vl-make-list-of-bitselects (vl-expr-fix expr) low high) (vl-make-list-of-bitselects expr low high)))
Theorem:
(defthm vl-make-list-of-bitselects-vl-expr-equiv-congruence-on-expr (implies (vl-expr-equiv expr expr-equiv) (equal (vl-make-list-of-bitselects expr low high) (vl-make-list-of-bitselects expr-equiv low high))) :rule-classes :congruence)
Theorem:
(defthm vl-make-list-of-bitselects-of-nfix-low (equal (vl-make-list-of-bitselects expr (nfix low) high) (vl-make-list-of-bitselects expr low high)))
Theorem:
(defthm vl-make-list-of-bitselects-nat-equiv-congruence-on-low (implies (acl2::nat-equiv low low-equiv) (equal (vl-make-list-of-bitselects expr low high) (vl-make-list-of-bitselects expr low-equiv high))) :rule-classes :congruence)
Theorem:
(defthm vl-make-list-of-bitselects-of-nfix-high (equal (vl-make-list-of-bitselects expr low (nfix high)) (vl-make-list-of-bitselects expr low high)))
Theorem:
(defthm vl-make-list-of-bitselects-nat-equiv-congruence-on-high (implies (acl2::nat-equiv high high-equiv) (equal (vl-make-list-of-bitselects expr low high) (vl-make-list-of-bitselects expr low high-equiv))) :rule-classes :congruence)