Explode a
(vl-msb-bitslice-partselect x ss warnings) → (mv successp warnings bit-exprs)
We require that
The list of bits we want to return here depends on the order of the msb and lsb indices for the wire. To consider the cases, imagine:
wire [3:0] a; wire [0:3] b;
There are four kinds of selects we might encounter, basically:
Function:
(defun vl-msb-bitslice-partselect (x ss warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (not (vl-atom-p x)) (equal (vl-nonatom->op x) :vl-partselect-colon) (vl-expr-welltyped-p x) (vl-expr-sliceable-p x)))) (let ((__function__ 'vl-msb-bitslice-partselect)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) (args (vl-nonatom->args x)) (from (first args)) (left (second args)) (right (third args)) (left-val (vl-resolved->val left)) (right-val (vl-resolved->val right)) ((mv warning range) (vl-ss-find-hidexpr-range from ss)) ((when warning) (mv nil (fatal :type :vl-slicing-fail :msg "Expected a net/reg declaration for ~a0." :args (list x)) nil)) ((unless (vl-maybe-range-resolved-p range)) (mv nil (fatal :type :vl-slicing-fail :msg "Expected the range of ~a0 to be resolved, but it ~ is ~a1." :args (list x range)) nil)) ((unless range) (mv nil (fatal :type :vl-slicing-fail :msg "Trying to do a part-select, ~a0, but ~a1 does not ~ have a range." :args (list x from)) nil)) ((vl-range range) range) (wire-msb-val (vl-resolved->val range.msb)) (wire-lsb-val (vl-resolved->val range.lsb)) (wire-is-msb-first-p (>= wire-msb-val wire-lsb-val)) (select-is-msb-first-p (>= left-val right-val)) (select-is-trivial-p (= left-val right-val)) ((unless (or (equal wire-is-msb-first-p select-is-msb-first-p) select-is-trivial-p)) (mv nil (fatal :type :vl-slicing-fail :msg "Trying to do a part-select, ~a0, in the opposite ~ order of the range from ~a1 (~a2)." :args (list x from range)) nil)) (wire-max (max wire-msb-val wire-lsb-val)) (wire-min (min wire-msb-val wire-lsb-val)) (sel-max (max left-val right-val)) (sel-min (min left-val right-val)) ((unless (and (<= wire-min sel-min) (<= sel-max wire-max))) (mv nil (fatal :type :vl-slicing-fail :msg "Part select ~a0 is out of bounds; the range of ~a1 ~ is only ~a2." :args (list x from range)) nil)) (bits (vl-make-msb-to-lsb-bitselects from left-val right-val))) (mv t (ok) bits))))
Theorem:
(defthm booleanp-of-vl-msb-bitslice-partselect.successp (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-partselect x ss warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-msb-bitslice-partselect.warnings (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-partselect x ss warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-p-of-vl-msb-bitslice-partselect.bit-exprs (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-partselect x ss warnings))) (vl-exprlist-p bit-exprs)) :rule-classes :rewrite)
Theorem:
(defthm vl-msb-bitslice-partselect-mvtypes-0 (booleanp (mv-nth 0 (vl-msb-bitslice-partselect x ss warnings))) :rule-classes :type-prescription)
Theorem:
(defthm vl-msb-bitslice-partselect-mvtypes-2 (true-listp (mv-nth 2 (vl-msb-bitslice-partselect x ss warnings))) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-msb-bitslice-partselect (let ((ret (vl-msb-bitslice-partselect x ss warnings))) (implies (and (mv-nth 0 ret) (force (not (vl-atom-p x))) (force (equal (vl-nonatom->op x) :vl-partselect-colon)) (force (vl-expr-welltyped-p x))) (equal (len (mv-nth 2 ret)) (vl-nonatom->finalwidth x)))))
Theorem:
(defthm vl-exprlist->finalwidths-of-vl-msb-bitslice-partselect (let ((ret (vl-msb-bitslice-partselect x ss warnings))) (implies (and (mv-nth 0 ret) (force (not (vl-atom-p x))) (force (equal (vl-nonatom->op x) :vl-partselect-colon)) (force (vl-expr-welltyped-p x))) (equal (vl-exprlist->finalwidths (mv-nth 2 ret)) (replicate (vl-nonatom->finalwidth x) 1)))))
Theorem:
(defthm vl-exprlist->finaltypes-of-vl-msb-bitslice-partselect (let ((ret (vl-msb-bitslice-partselect x ss warnings))) (implies (and (mv-nth 0 ret) (force (not (vl-atom-p x))) (force (equal (vl-nonatom->op x) :vl-partselect-colon)) (force (vl-expr-welltyped-p x))) (equal (vl-exprlist->finaltypes (mv-nth 2 ret)) (replicate (vl-nonatom->finalwidth x) :vl-unsigned)))))
Theorem:
(defthm vl-exprlist-welltyped-p-of-vl-msb-bitslice-partselect (let ((ret (vl-msb-bitslice-partselect x ss warnings))) (implies (and (mv-nth 0 ret) (force (not (vl-atom-p x))) (force (equal (vl-nonatom->op x) :vl-partselect-colon)) (force (vl-expr-welltyped-p x))) (vl-exprlist-welltyped-p (mv-nth 2 ret)))))
Theorem:
(defthm vl-msb-bitslice-partselect-of-vl-expr-fix-x (equal (vl-msb-bitslice-partselect (vl-expr-fix x) ss warnings) (vl-msb-bitslice-partselect x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-partselect-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-msb-bitslice-partselect x ss warnings) (vl-msb-bitslice-partselect x-equiv ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bitslice-partselect-of-vl-scopestack-fix-ss (equal (vl-msb-bitslice-partselect x (vl-scopestack-fix ss) warnings) (vl-msb-bitslice-partselect x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-partselect-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-msb-bitslice-partselect x ss warnings) (vl-msb-bitslice-partselect x ss-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bitslice-partselect-of-vl-warninglist-fix-warnings (equal (vl-msb-bitslice-partselect x ss (vl-warninglist-fix warnings)) (vl-msb-bitslice-partselect x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-partselect-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-msb-bitslice-partselect x ss warnings) (vl-msb-bitslice-partselect x ss warnings-equiv))) :rule-classes :congruence)