		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-index-shift-amount

Signature
(vl-index-shift-amount size msb lsb idx) → shift
Arguments: size — Guard (natp size).; msb — Guard (integerp msb).; lsb — Guard (integerp lsb).; idx — Guard (sv::svex-p idx).
Returns: shift — Type (implies (not err) (sv::svex-p shift)).

Definitions and Theorems

Function: vl-index-shift-amount

(defun vl-index-shift-amount (size msb lsb idx)
 (declare (xargs :guard (and (natp size)
                             (integerp msb)
                             (integerp lsb)
                             (sv::svex-p idx))))
 (let ((__function__ 'vl-index-shift-amount))
   (declare (ignorable __function__))
   (b* ((size (lnfix size))
        (msb (lifix msb))
        (lsb (lifix lsb))
        ((when (>= msb lsb))
         (sv::svex-reduce-consts
              (sv::svcall * (svex-int size)
                          (sv::svcall sv::b- idx (svex-int lsb))))))
     (sv::svex-reduce-consts
          (sv::svcall * (svex-int size)
                      (sv::svcall sv::b- (svex-int lsb)
                                  idx))))))

Theorem: return-type-of-vl-index-shift-amount

(defthm return-type-of-vl-index-shift-amount
  (b* ((shift (vl-index-shift-amount size msb lsb idx)))
    (implies (not err) (sv::svex-p shift)))
  :rule-classes :rewrite)

Theorem: vars-of-vl-index-shift-amount

(defthm vars-of-vl-index-shift-amount
  (b* ((?shift (vl-index-shift-amount size msb lsb idx)))
    (implies (not (member v (sv::svex-vars idx)))
             (not (member v (sv::svex-vars shift))))))

Theorem: vl-index-shift-amount-of-nfix-size

(defthm vl-index-shift-amount-of-nfix-size
  (equal (vl-index-shift-amount (nfix size)
                                msb lsb idx)
         (vl-index-shift-amount size msb lsb idx)))

Theorem: vl-index-shift-amount-nat-equiv-congruence-on-size

(defthm vl-index-shift-amount-nat-equiv-congruence-on-size
  (implies (acl2::nat-equiv size size-equiv)
           (equal (vl-index-shift-amount size msb lsb idx)
                  (vl-index-shift-amount size-equiv msb lsb idx)))
  :rule-classes :congruence)

Theorem: vl-index-shift-amount-of-ifix-msb

(defthm vl-index-shift-amount-of-ifix-msb
  (equal (vl-index-shift-amount size (ifix msb)
                                lsb idx)
         (vl-index-shift-amount size msb lsb idx)))

Theorem: vl-index-shift-amount-int-equiv-congruence-on-msb

(defthm vl-index-shift-amount-int-equiv-congruence-on-msb
  (implies (acl2::int-equiv msb msb-equiv)
           (equal (vl-index-shift-amount size msb lsb idx)
                  (vl-index-shift-amount size msb-equiv lsb idx)))
  :rule-classes :congruence)

Theorem: vl-index-shift-amount-of-ifix-lsb

(defthm vl-index-shift-amount-of-ifix-lsb
  (equal (vl-index-shift-amount size msb (ifix lsb)
                                idx)
         (vl-index-shift-amount size msb lsb idx)))

Theorem: vl-index-shift-amount-int-equiv-congruence-on-lsb

(defthm vl-index-shift-amount-int-equiv-congruence-on-lsb
  (implies (acl2::int-equiv lsb lsb-equiv)
           (equal (vl-index-shift-amount size msb lsb idx)
                  (vl-index-shift-amount size msb lsb-equiv idx)))
  :rule-classes :congruence)

Theorem: vl-index-shift-amount-of-svex-fix-idx

(defthm vl-index-shift-amount-of-svex-fix-idx
  (equal (vl-index-shift-amount size msb lsb (sv::svex-fix idx))
         (vl-index-shift-amount size msb lsb idx)))

Theorem: vl-index-shift-amount-svex-equiv-congruence-on-idx

(defthm vl-index-shift-amount-svex-equiv-congruence-on-idx
  (implies (sv::svex-equiv idx idx-equiv)
           (equal (vl-index-shift-amount size msb lsb idx)
                  (vl-index-shift-amount size msb lsb idx-equiv)))
  :rule-classes :congruence)