Converts MSB-first digits into an initial (not truncated, not extended) MSB-first vl-bitlist-p.
(vl-hex-digits-to-bitlist digits) → bits
Function:
(defun vl-hex-digits-to-bitlist (digits) (declare (xargs :guard (character-listp digits))) (let ((__function__ 'vl-hex-digits-to-bitlist)) (declare (ignorable __function__)) (if (atom digits) nil (append (case (car digits) (#\0 (list :vl-0val :vl-0val :vl-0val :vl-0val)) (#\1 (list :vl-0val :vl-0val :vl-0val :vl-1val)) (#\2 (list :vl-0val :vl-0val :vl-1val :vl-0val)) (#\3 (list :vl-0val :vl-0val :vl-1val :vl-1val)) (#\4 (list :vl-0val :vl-1val :vl-0val :vl-0val)) (#\5 (list :vl-0val :vl-1val :vl-0val :vl-1val)) (#\6 (list :vl-0val :vl-1val :vl-1val :vl-0val)) (#\7 (list :vl-0val :vl-1val :vl-1val :vl-1val)) (#\8 (list :vl-1val :vl-0val :vl-0val :vl-0val)) (#\9 (list :vl-1val :vl-0val :vl-0val :vl-1val)) ((#\A #\a) (list :vl-1val :vl-0val :vl-1val :vl-0val)) ((#\B #\b) (list :vl-1val :vl-0val :vl-1val :vl-1val)) ((#\C #\c) (list :vl-1val :vl-1val :vl-0val :vl-0val)) ((#\D #\d) (list :vl-1val :vl-1val :vl-0val :vl-1val)) ((#\E #\e) (list :vl-1val :vl-1val :vl-1val :vl-0val)) ((#\F #\f) (list :vl-1val :vl-1val :vl-1val :vl-1val)) ((#\x #\X) (list :vl-xval :vl-xval :vl-xval :vl-xval)) ((#\z #\Z #\?) (list :vl-zval :vl-zval :vl-zval :vl-zval)) (otherwise (progn$ (raise "Not a hex digit: ~x0.~%" (car digits)) (list :vl-0val :vl-0val :vl-0val :vl-0val)))) (vl-hex-digits-to-bitlist (cdr digits))))))
Theorem:
(defthm vl-bitlist-p-of-vl-hex-digits-to-bitlist (b* ((bits (vl-hex-digits-to-bitlist digits))) (vl-bitlist-p bits)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-hex-digits-to-bitlist (equal (len (vl-hex-digits-to-bitlist x)) (* 4 (len x))))