		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-pow

Power operator (** in SystemVerilog).

Signature
(4vec-pow base exp) → res
Arguments: base — Guard (4vec-p base).; exp — Guard (4vec-p exp).
Returns: res — Type (4vec-p res).

See Table 11-4 in IEEE System Verilog Spec.

Definitions and Theorems

Function: 4vec-pow

(defun 4vec-pow (base exp)
  (declare (xargs :guard (and (4vec-p base) (4vec-p exp))))
  (let ((__function__ '4vec-pow))
    (declare (ignorable __function__))
    (if (and (2vec-p base) (2vec-p exp))
        (b* ((base (2vec->val base))
             (exp (2vec->val exp))
             ((when (or (natp exp)
                        (eql base 1)
                        (eql base -1)))
              (2vec (expt base exp)))
             ((when (eql base 0)) (4vec-x)))
          (2vec 0))
      (4vec-x))))

Theorem: 4vec-p-of-4vec-pow

(defthm 4vec-p-of-4vec-pow
  (b* ((res (4vec-pow base exp)))
    (4vec-p res))
  :rule-classes :rewrite)

Theorem: 4vec-pow-of-2vecx-fix-base

(defthm 4vec-pow-of-2vecx-fix-base
  (equal (4vec-pow (2vecx-fix base) exp)
         (4vec-pow base exp)))

Theorem: 4vec-pow-2vecx-equiv-congruence-on-base

(defthm 4vec-pow-2vecx-equiv-congruence-on-base
  (implies (2vecx-equiv base base-equiv)
           (equal (4vec-pow base exp)
                  (4vec-pow base-equiv exp)))
  :rule-classes :congruence)

Theorem: 4vec-pow-of-2vecx-fix-exp

(defthm 4vec-pow-of-2vecx-fix-exp
  (equal (4vec-pow base (2vecx-fix exp))
         (4vec-pow base exp)))

Theorem: 4vec-pow-2vecx-equiv-congruence-on-exp

(defthm 4vec-pow-2vecx-equiv-congruence-on-exp
  (implies (2vecx-equiv exp exp-equiv)
           (equal (4vec-pow base exp)
                  (4vec-pow base exp-equiv)))
  :rule-classes :congruence)