Safely create the bit-select
Historic note. We used to (incorrectly) check whether N was less than the final-width of the expression, and also optimize so that when FOO had width 1, we would create FOO instead of FOO[0]. This did not cause problems since this function was only used in occform (where the wires we were generating always started at index 0), but is more generally incorrect since a wire's finalwidth need not be related to the valid bits that can be selected from it, e.g., wire [7:5] w; should allow us to select w[7], w[6], and w[5], but the width of w is only 2.
We no longer try to do any bounds-checking here, since it is really not possible to do it correctly without knowing the bounds of the wire, which is not available to us here. You can hence use this function to create an invalid expression like foo[n]; garbage in, garbage out.
Function:
(defun vl-make-bitselect (expr n) (declare (xargs :guard (and (vl-expr-p expr) (natp n)))) (let ((__function__ 'vl-make-bitselect)) (declare (ignorable __function__)) (b* (((unless (vl-fast-atom-p expr)) (raise "Trying to select from non-atom: ~x0." expr) |*sized-1'b0*|) ((unless (posp (vl-expr->finalwidth expr))) (raise "Trying to select from unwidthed expr: ~x0" expr) |*sized-1'b0*|) (guts (vl-atom->guts expr)) ((unless (vl-id-p guts)) (raise "Not implemented: bitselect from ~x0." (tag guts)) |*sized-1'b0*|)) (hons-copy (make-vl-nonatom :op :vl-bitselect :args (acl2::hons-list (vl-expr-fix expr) (vl-make-index n)) :finalwidth 1 :finaltype :vl-unsigned)))))
Theorem:
(defthm vl-expr-p-of-vl-make-bitselect (b* ((expr[n] (vl-make-bitselect expr n))) (vl-expr-p expr[n])) :rule-classes :rewrite)
Theorem:
(defthm vl-expr->finalwidth-of-vl-make-bitselect (equal (vl-expr->finalwidth (vl-make-bitselect expr n)) 1))
Theorem:
(defthm vl-expr->finaltype-of-vl-make-bitselect (equal (vl-expr->finaltype (vl-make-bitselect expr n)) :vl-unsigned))
Theorem:
(defthm vl-make-bitselect-of-vl-expr-fix-expr (equal (vl-make-bitselect (vl-expr-fix expr) n) (vl-make-bitselect expr n)))
Theorem:
(defthm vl-make-bitselect-vl-expr-equiv-congruence-on-expr (implies (vl-expr-equiv expr expr-equiv) (equal (vl-make-bitselect expr n) (vl-make-bitselect expr-equiv n))) :rule-classes :congruence)
Theorem:
(defthm vl-make-bitselect-of-nfix-n (equal (vl-make-bitselect expr (nfix n)) (vl-make-bitselect expr n)))
Theorem:
(defthm vl-make-bitselect-nat-equiv-congruence-on-n (implies (acl2::nat-equiv n n-equiv) (equal (vl-make-bitselect expr n) (vl-make-bitselect expr n-equiv))) :rule-classes :congruence)