		Search-engine friendly clone of the ACL2 documentation.

Selfassigns

Vl-selfassign-bits

Signature
(vl-selfassign-bits name low high) → bits
Arguments: name — Guard (stringp name).; low — Guard (integerp low).; high — Guard (integerp high).
Returns: bits — Type (string-listp bits).

Definitions and Theorems

Function: vl-selfassign-bits

(defun vl-selfassign-bits (name low high)
  (declare (xargs :guard (and (stringp name)
                              (integerp low)
                              (integerp high))))
  (declare (xargs :guard (<= low high)))
  (let ((__function__ 'vl-selfassign-bits))
    (declare (ignorable __function__))
    (if (mbe :logic (zp (- (ifix high) (ifix low)))
             :exec (eql high low))
        (list (vl-selfassign-bit name low))
      (cons (vl-selfassign-bit name low)
            (vl-selfassign-bits name (+ (lifix low) 1)
                                high)))))

Theorem: string-listp-of-vl-selfassign-bits

(defthm string-listp-of-vl-selfassign-bits
  (b* ((bits (vl-selfassign-bits name low high)))
    (string-listp bits))
  :rule-classes :rewrite)

Theorem: vl-selfassign-bits-of-str-fix-name

(defthm vl-selfassign-bits-of-str-fix-name
  (equal (vl-selfassign-bits (str-fix name)
                             low high)
         (vl-selfassign-bits name low high)))

Theorem: vl-selfassign-bits-streqv-congruence-on-name

(defthm vl-selfassign-bits-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-selfassign-bits name low high)
                  (vl-selfassign-bits name-equiv low high)))
  :rule-classes :congruence)

Theorem: vl-selfassign-bits-of-ifix-low

(defthm vl-selfassign-bits-of-ifix-low
  (equal (vl-selfassign-bits name (ifix low)
                             high)
         (vl-selfassign-bits name low high)))

Theorem: vl-selfassign-bits-int-equiv-congruence-on-low

(defthm vl-selfassign-bits-int-equiv-congruence-on-low
  (implies (acl2::int-equiv low low-equiv)
           (equal (vl-selfassign-bits name low high)
                  (vl-selfassign-bits name low-equiv high)))
  :rule-classes :congruence)

Theorem: vl-selfassign-bits-of-ifix-high

(defthm vl-selfassign-bits-of-ifix-high
  (equal (vl-selfassign-bits name low (ifix high))
         (vl-selfassign-bits name low high)))

Theorem: vl-selfassign-bits-int-equiv-congruence-on-high

(defthm vl-selfassign-bits-int-equiv-congruence-on-high
  (implies (acl2::int-equiv high high-equiv)
           (equal (vl-selfassign-bits name low high)
                  (vl-selfassign-bits name low high-equiv)))
  :rule-classes :congruence)