Produce an MSB-ordered list of the bits for some value.
(vl-msb-constint-bitlist-aux value acc) → *
Function:
(defun vl-msb-constint-bitlist-aux (value acc) (declare (xargs :guard (natp value))) (let ((__function__ 'vl-msb-constint-bitlist-aux)) (declare (ignorable __function__)) (b* (((when (zp value)) acc) (floor2 (mbe :logic (floor value 2) :exec (ash value -1))) (mod2 (mbe :logic (mod value 2) :exec (rem value 2))) (bit (if (eql mod2 0) 'acl2::f 't))) (vl-msb-constint-bitlist-aux floor2 (cons bit acc)))))
Theorem:
(defthm true-listp-of-vl-msb-constint-bitlist-aux (implies (true-listp acc) (true-listp (vl-msb-constint-bitlist-aux value acc))) :rule-classes :type-prescription)
Theorem:
(defthm vl-emodwirelist-p-of-vl-msb-constint-bitlist-aux (implies (vl-emodwirelist-p acc) (vl-emodwirelist-p (vl-msb-constint-bitlist-aux value acc))))