		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-size-to-unsigned-logic

Signature
(vl-size-to-unsigned-logic x) → type
Arguments: x — Guard (posp x).
Returns: type — Type (vl-datatype-p type).

Definitions and Theorems

Function: vl-size-to-unsigned-logic

(defun vl-size-to-unsigned-logic (x)
 (declare (xargs :guard (posp x)))
 (let ((__function__ 'vl-size-to-unsigned-logic))
  (declare (ignorable __function__))
  (hons-copy
   (make-vl-coretype
     :name :vl-logic
     :pdims
     (list (vl-range->dimension
                (make-vl-range :msb (vl-make-index (1- (pos-fix x)))
                               :lsb (vl-make-index 0))))))))

Theorem: vl-datatype-p-of-vl-size-to-unsigned-logic

(defthm vl-datatype-p-of-vl-size-to-unsigned-logic
  (b* ((type (vl-size-to-unsigned-logic x)))
    (vl-datatype-p type))
  :rule-classes :rewrite)

Theorem: vl-size-to-unsigned-logic-type-ok

(defthm vl-size-to-unsigned-logic-type-ok
  (b* ((common-lisp::?type (vl-size-to-unsigned-logic x)))
    (vl-datatype-resolved-p type)))

Theorem: vl-size-to-unsigned-logic-of-pos-fix-x

(defthm vl-size-to-unsigned-logic-of-pos-fix-x
  (equal (vl-size-to-unsigned-logic (pos-fix x))
         (vl-size-to-unsigned-logic x)))

Theorem: vl-size-to-unsigned-logic-pos-equiv-congruence-on-x

(defthm vl-size-to-unsigned-logic-pos-equiv-congruence-on-x
  (implies (acl2::pos-equiv x x-equiv)
           (equal (vl-size-to-unsigned-logic x)
                  (vl-size-to-unsigned-logic x-equiv)))
  :rule-classes :congruence)