Convert an
(vl-decimal-digits-to-bitlist digits) → bits
See vl-read-decimal-value. The only time this should be called is if digits is a singleton list containing exactly the digit x or z.
Function:
(defun vl-decimal-digits-to-bitlist (digits) (declare (xargs :guard (character-listp digits))) (let ((__function__ 'vl-decimal-digits-to-bitlist)) (declare (ignorable __function__)) (cond ((member-equal digits (list '(#\x) '(#\X))) (list :vl-xval)) ((member-equal digits (list '(#\z) '(#\Z) '(#\?))) (list :vl-zval)) (t (progn$ (raise "Programming error") (list :vl-xval))))))
Theorem:
(defthm vl-bitlist-p-of-vl-decimal-digits-to-bitlist (b* ((bits (vl-decimal-digits-to-bitlist digits))) (vl-bitlist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-decimal-digits-to-bitlist (equal (len (vl-decimal-digits-to-bitlist x)) 1))