Explode a
(vl-msb-bitslice-weirdint x) → bit-exprs
We require that
Note that the bits of a weirdint are already in msb-first order, so we just need to convert them into individual bits in the same order.
Function:
(defun vl-msb-bitslice-weirdint (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (and (vl-atom-p x) (vl-atom-welltyped-p x) (vl-fast-weirdint-p (vl-atom->guts x))))) (let ((__function__ 'vl-msb-bitslice-weirdint)) (declare (ignorable __function__)) (vl-bitlist-to-sized-exprs (vl-weirdint->bits (vl-atom->guts x)))))
Theorem:
(defthm vl-exprlist-p-of-vl-msb-bitslice-weirdint (b* ((bit-exprs (vl-msb-bitslice-weirdint x))) (vl-exprlist-p bit-exprs)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-msb-bitslice-weirdint (true-listp (vl-msb-bitslice-weirdint x)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-msb-bitslice-weirdint (implies (and (force (vl-atom-p x)) (force (vl-atom-welltyped-p x)) (force (vl-weirdint-p (vl-atom->guts x)))) (equal (len (vl-msb-bitslice-weirdint x)) (vl-atom->finalwidth x))))
Theorem:
(defthm vl-exprlist->finalwidths-of-vl-msb-bitslice-weirdint (implies (and (force (vl-atom-p x)) (force (vl-atom-welltyped-p x)) (force (vl-weirdint-p (vl-atom->guts x)))) (equal (vl-exprlist->finalwidths (vl-msb-bitslice-weirdint x)) (replicate (vl-atom->finalwidth x) 1))))
Theorem:
(defthm vl-exprlist->finaltypes-of-vl-msb-bitslice-weirdint (implies (and (force (vl-atom-p x)) (force (vl-atom-welltyped-p x)) (force (vl-weirdint-p (vl-atom->guts x)))) (equal (vl-exprlist->finaltypes (vl-msb-bitslice-weirdint x)) (replicate (vl-atom->finalwidth x) :vl-unsigned))))
Theorem:
(defthm vl-exprlist-welltyped-p-of-vl-msb-bitslice-weirdint (vl-exprlist-welltyped-p (vl-msb-bitslice-weirdint x)))
Theorem:
(defthm vl-msb-bitslice-weirdint-of-vl-expr-fix-x (equal (vl-msb-bitslice-weirdint (vl-expr-fix x)) (vl-msb-bitslice-weirdint x)))
Theorem:
(defthm vl-msb-bitslice-weirdint-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-msb-bitslice-weirdint x) (vl-msb-bitslice-weirdint x-equiv))) :rule-classes :congruence)