		Search-engine friendly clone of the ACL2 documentation.

Weirdint-elim

Vl-weirdint-bits-to-exprs

Translate MSB-first bits from a weirdint into expressions, which will become the arguments to a concatenation.

Signature
(vl-weirdint-bits-to-exprs bits) → exprs
Arguments: bits — Guard (vl-bitlist-p bits).
Returns: exprs — Any 0 bits become 1'b0, 1 bits become 1'b1, Z bits become vl-z-wire, and X bits become vl-x-wire.
Type (vl-exprlist-p exprs).

Definitions and Theorems

Function: vl-weirdint-bits-to-exprs

(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: vl-exprlist-p-of-vl-weirdint-bits-to-exprs

(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: vl-weirdint-bits-to-exprs-of-vl-bitlist-fix-bits

(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: vl-weirdint-bits-to-exprs-vl-bitlist-equiv-congruence-on-bits

(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)