Convert MSB-first binary digits into an initial (not truncated, not extended) MSB-first vl-bitlist-p.
(vl-binary-digits-to-bitlist digits) → bits
Function:
(defun vl-binary-digits-to-bitlist (digits) (declare (xargs :guard (character-listp digits))) (let ((__function__ 'vl-binary-digits-to-bitlist)) (declare (ignorable __function__)) (if (atom digits) nil (cons (case (car digits) (#\0 :vl-0val) (#\1 :vl-1val) ((#\x #\X) :vl-xval) ((#\z #\Z #\?) :vl-zval) (otherwise (progn$ (raise "Not a binary digit: ~x0.~%" (car digits)) :vl-0val))) (vl-binary-digits-to-bitlist (cdr digits))))))
Theorem:
(defthm vl-bitlist-p-of-vl-binary-digits-to-bitlist (b* ((bits (vl-binary-digits-to-bitlist digits))) (vl-bitlist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-binary-digits-to-bitlist (equal (len (vl-binary-digits-to-bitlist x)) (len x)))