Explode a
(vl-msb-bitslice-hidexpr 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. For instance, if the wire is declared as:
wire [3:0] w;
Then we want to return
wire [0:3] w;
Then we will want to return
Function:
(defun vl-msb-bitslice-hidexpr (x ss warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (vl-hidexpr-p x) (or (vl-atom-p x) (eq (vl-nonatom->op x) :vl-hid-dot)) (vl-expr-welltyped-p x)))) (let ((__function__ 'vl-msb-bitslice-hidexpr)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) ((mv successp warnings main-bits) (vl-msb-bitslice-hidexpr-base x ss warnings)) ((unless successp) (mv nil warnings nil)) (x.finalwidth (vl-expr->finalwidth x)) (x.finaltype (vl-expr->finaltype x)) (nwires (len main-bits)) ((when (< x.finalwidth nwires)) (mv nil (fatal :type :vl-programming-error :msg "Found an identifier/HID expression for ~a0 ~ with width ~x1, which is smaller than ~x2, the size ~ of its range. Expected all occurrences of plain ~ identifiers to have widths that are at least as ~ large as their declarations." :args (list x x.finalwidth nwires)) nil)) ((when (eql nwires x.finalwidth)) (mv t warnings main-bits)) (extension-bit (if (eq x.finaltype :vl-signed) (car main-bits) |*sized-1'b0*|)) (bits (append (replicate (- x.finalwidth nwires) extension-bit) main-bits))) (mv t warnings bits))))
Theorem:
(defthm booleanp-of-vl-msb-bitslice-hidexpr.successp (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-hidexpr x ss warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-msb-bitslice-hidexpr.warnings (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-hidexpr x ss warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-p-of-vl-msb-bitslice-hidexpr.bit-exprs (b* (((mv ?successp ?warnings ?bit-exprs) (vl-msb-bitslice-hidexpr x ss warnings))) (vl-exprlist-p bit-exprs)) :rule-classes :rewrite)
Theorem:
(defthm vl-msb-bitslice-hidexpr-mvtypes-0 (booleanp (mv-nth 0 (vl-msb-bitslice-hidexpr x ss warnings))) :rule-classes :type-prescription)
Theorem:
(defthm vl-msb-bitslice-hidexpr-mvtypes-2 (true-listp (mv-nth 2 (vl-msb-bitslice-hidexpr x ss warnings))) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-msb-bitslice-hidexpr (let ((ret (vl-msb-bitslice-hidexpr x ss warnings))) (implies (and (mv-nth 0 ret) (force (vl-hidexpr-p x)) (force (vl-expr-welltyped-p x))) (equal (len (mv-nth 2 ret)) (vl-expr->finalwidth x)))))
Theorem:
(defthm vl-exprlist->finalwidths-of-vl-msb-bitslice-hidexpr (let ((ret (vl-msb-bitslice-hidexpr x ss warnings))) (implies (and (mv-nth 0 ret) (force (vl-hidexpr-p x)) (force (vl-expr-welltyped-p x))) (equal (vl-exprlist->finalwidths (mv-nth 2 ret)) (replicate (vl-expr->finalwidth x) 1)))))
Theorem:
(defthm vl-exprlist->finaltypes-of-vl-msb-bitslice-hidexpr (let ((ret (vl-msb-bitslice-hidexpr x ss warnings))) (implies (and (mv-nth 0 ret) (force (vl-hidexpr-p x)) (force (vl-expr-welltyped-p x))) (equal (vl-exprlist->finaltypes (mv-nth 2 ret)) (replicate (vl-expr->finalwidth x) :vl-unsigned)))))
Theorem:
(defthm vl-exprlist-welltyped-p-of-vl-msb-bitslice-hidexpr (let ((ret (vl-msb-bitslice-hidexpr x ss warnings))) (implies (and (mv-nth 0 ret) (force (vl-hidexpr-p x)) (or (vl-atom-p x) (eq (vl-nonatom->op x) :vl-hid-dot)) (force (vl-expr-welltyped-p x))) (vl-exprlist-welltyped-p (mv-nth 2 ret)))))
Theorem:
(defthm vl-msb-bitslice-hidexpr-of-vl-expr-fix-x (equal (vl-msb-bitslice-hidexpr (vl-expr-fix x) ss warnings) (vl-msb-bitslice-hidexpr x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-hidexpr-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-msb-bitslice-hidexpr x ss warnings) (vl-msb-bitslice-hidexpr x-equiv ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bitslice-hidexpr-of-vl-scopestack-fix-ss (equal (vl-msb-bitslice-hidexpr x (vl-scopestack-fix ss) warnings) (vl-msb-bitslice-hidexpr x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-hidexpr-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-msb-bitslice-hidexpr x ss warnings) (vl-msb-bitslice-hidexpr x ss-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-msb-bitslice-hidexpr-of-vl-warninglist-fix-warnings (equal (vl-msb-bitslice-hidexpr x ss (vl-warninglist-fix warnings)) (vl-msb-bitslice-hidexpr x ss warnings)))
Theorem:
(defthm vl-msb-bitslice-hidexpr-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-msb-bitslice-hidexpr x ss warnings) (vl-msb-bitslice-hidexpr x ss warnings-equiv))) :rule-classes :congruence)