Build a list of expressions,
(vl-make-msb-to-lsb-bitselects expr msb lsb) → selects
Function:
(defun vl-make-msb-to-lsb-bitselects (expr msb lsb) (declare (xargs :guard (and (vl-expr-p expr) (natp msb) (natp lsb)))) (let ((__function__ 'vl-make-msb-to-lsb-bitselects)) (declare (ignorable __function__)) (b* ((msb (lnfix msb)) (lsb (lnfix lsb)) (left-right-p (>= msb lsb)) (low (if left-right-p lsb msb)) (high (if left-right-p msb lsb)) (list (vl-make-list-of-bitselects expr low high))) (if left-right-p (reverse list) list))))
Theorem:
(defthm vl-exprlist-p-of-vl-make-msb-to-lsb-bitselects (b* ((selects (vl-make-msb-to-lsb-bitselects expr msb lsb))) (vl-exprlist-p selects)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-make-msb-to-lsb-bitselects (true-listp (vl-make-msb-to-lsb-bitselects expr msb lsb)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-make-msb-to-lsb-bitselects (equal (len (vl-make-msb-to-lsb-bitselects expr msb lsb)) (+ 1 (abs (- (nfix msb) (nfix lsb))))))
Theorem:
(defthm vl-exprlist->finalwidths-of-vl-make-msb-to-lsb-bitselects (equal (vl-exprlist->finalwidths (vl-make-msb-to-lsb-bitselects expr msb lsb)) (replicate (+ 1 (abs (- (nfix msb) (nfix lsb)))) 1)))
Theorem:
(defthm vl-exprlist->finaltypes-of-vl-make-msb-to-lsb-bitselects (equal (vl-exprlist->finaltypes (vl-make-msb-to-lsb-bitselects expr msb lsb)) (replicate (+ 1 (abs (- (nfix msb) (nfix lsb)))) :vl-unsigned)))
Theorem:
(defthm vl-make-msb-to-lsb-bitselects-of-vl-expr-fix-expr (equal (vl-make-msb-to-lsb-bitselects (vl-expr-fix expr) msb lsb) (vl-make-msb-to-lsb-bitselects expr msb lsb)))
Theorem:
(defthm vl-make-msb-to-lsb-bitselects-vl-expr-equiv-congruence-on-expr (implies (vl-expr-equiv expr expr-equiv) (equal (vl-make-msb-to-lsb-bitselects expr msb lsb) (vl-make-msb-to-lsb-bitselects expr-equiv msb lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-make-msb-to-lsb-bitselects-of-nfix-msb (equal (vl-make-msb-to-lsb-bitselects expr (nfix msb) lsb) (vl-make-msb-to-lsb-bitselects expr msb lsb)))
Theorem:
(defthm vl-make-msb-to-lsb-bitselects-nat-equiv-congruence-on-msb (implies (acl2::nat-equiv msb msb-equiv) (equal (vl-make-msb-to-lsb-bitselects expr msb lsb) (vl-make-msb-to-lsb-bitselects expr msb-equiv lsb))) :rule-classes :congruence)
Theorem:
(defthm vl-make-msb-to-lsb-bitselects-of-nfix-lsb (equal (vl-make-msb-to-lsb-bitselects expr msb (nfix lsb)) (vl-make-msb-to-lsb-bitselects expr msb lsb)))
Theorem:
(defthm vl-make-msb-to-lsb-bitselects-nat-equiv-congruence-on-lsb (implies (acl2::nat-equiv lsb lsb-equiv) (equal (vl-make-msb-to-lsb-bitselects expr msb lsb) (vl-make-msb-to-lsb-bitselects expr msb lsb-equiv))) :rule-classes :congruence)