(vl-lsb-bitslice-constint-aux len value) → exprs
Function:
(defun vl-lsb-bitslice-constint-aux (len value) (declare (xargs :guard (and (natp len) (natp value)))) (let ((__function__ 'vl-lsb-bitslice-constint-aux)) (declare (ignorable __function__)) (b* (((when (zp len)) nil) (floor2 (mbe :logic (floor (nfix value) 2) :exec (ash value -1))) (mod2 (mbe :logic (mod (nfix value) 2) :exec (logand value 1))) (bit (if (eql mod2 0) |*sized-1'b0*| |*sized-1'b1*|))) (cons bit (vl-lsb-bitslice-constint-aux (mbe :logic (- (nfix len) 1) :exec (- len 1)) floor2)))))
Theorem:
(defthm vl-exprlist-p-of-vl-lsb-bitslice-constint-aux (b* ((exprs (vl-lsb-bitslice-constint-aux len value))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-lsb-bitslice-constint (true-listp (vl-lsb-bitslice-constint-aux len value)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-lsb-bitslice-constint-aux (equal (len (vl-lsb-bitslice-constint-aux len value)) (nfix len)))
Theorem:
(defthm vl-exprlist->finalwidths-of-vl-lsb-bitslice-constint-aux (equal (vl-exprlist->finalwidths (vl-lsb-bitslice-constint-aux len value)) (replicate (nfix len) 1)))
Theorem:
(defthm vl-exprlist->finaltypes-of-vl-lsb-bitslice-constint-aux (equal (vl-exprlist->finaltypes (vl-lsb-bitslice-constint-aux len value)) (replicate (nfix len) :vl-unsigned)))
Theorem:
(defthm vl-exprlist-welltyped-p-of-vl-lsb-bitslice-constint-aux (vl-exprlist-welltyped-p (vl-lsb-bitslice-constint-aux len value)))
Theorem:
(defthm vl-lsb-bitslice-constint-aux-of-nfix-len (equal (vl-lsb-bitslice-constint-aux (nfix len) value) (vl-lsb-bitslice-constint-aux len value)))
Theorem:
(defthm vl-lsb-bitslice-constint-aux-nat-equiv-congruence-on-len (implies (acl2::nat-equiv len len-equiv) (equal (vl-lsb-bitslice-constint-aux len value) (vl-lsb-bitslice-constint-aux len-equiv value))) :rule-classes :congruence)
Theorem:
(defthm vl-lsb-bitslice-constint-aux-of-nfix-value (equal (vl-lsb-bitslice-constint-aux len (nfix value)) (vl-lsb-bitslice-constint-aux len value)))
Theorem:
(defthm vl-lsb-bitslice-constint-aux-nat-equiv-congruence-on-value (implies (acl2::nat-equiv value value-equiv) (equal (vl-lsb-bitslice-constint-aux len value) (vl-lsb-bitslice-constint-aux len value-equiv))) :rule-classes :congruence)