Translate MSB-first bits from a weirdint into expressions, which will become the arguments to a concatenation.
(vl-weirdint-bits-to-exprs bits) → exprs
Function:
(defun vl-weirdint-bits-to-exprs (bits) (declare (xargs :guard (vl-bitlist-p bits))) (let ((__function__ 'vl-weirdint-bits-to-exprs)) (declare (ignorable __function__)) (if (atom bits) nil (cons (case (vl-bit-fix (car bits)) (:vl-0val |*sized-1'b0*|) (:vl-1val |*sized-1'b1*|) (:vl-xval *vl-x-wire-expr*) (:vl-zval *vl-z-wire-expr*)) (vl-weirdint-bits-to-exprs (cdr bits))))))
Theorem:
(defthm vl-exprlist-p-of-vl-weirdint-bits-to-exprs (b* ((exprs (vl-weirdint-bits-to-exprs bits))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm vl-weirdint-bits-to-exprs-of-vl-bitlist-fix-bits (equal (vl-weirdint-bits-to-exprs (vl-bitlist-fix bits)) (vl-weirdint-bits-to-exprs bits)))
Theorem:
(defthm vl-weirdint-bits-to-exprs-vl-bitlist-equiv-congruence-on-bits (implies (vl-bitlist-equiv bits bits-equiv) (equal (vl-weirdint-bits-to-exprs bits) (vl-weirdint-bits-to-exprs bits-equiv))) :rule-classes :congruence)