		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-parity

Reduction logical XOR (i.e., parity) of a 4vec.

Signature
(4vec-parity x) → parity
Arguments: x — Guard (4vec-p x).
Returns: parity — Type (3vec-p! parity).

We compute the parity of x if possible, following the boolean-convention. If x has any X or Z bits, or is a negative number, we just return all Xes. Otherwise, x is a natural number and we just return the parity of its 1 bits. For instance,

(4vec-parity #b0) == 0   (all 0s, false)
(4vec-parity #b1) == -1  (all 1s, true)
(4vec-parity #b11) == 0  (all 0s, false)
(4vec-parity #b10) == -1 (all 1s, true)

Subtle. Since 4vecs are ``infinite width,'' reduction operators are a bit unusual. For parity computations this is especially true for negative number: if x is negative, i.e., it has infinitely many leading 1 bits, it doesn't make much sense to ask about its parity. Accordingly, if you are translating from Verilog or other languages that have fixed width vectors, you will typically want to take the parity of, e.g., the 4vec-zero-ext of your vector.

Definitions and Theorems

Function: 4vec-parity

(defun 4vec-parity (x)
  (declare (xargs :guard (4vec-p x)))
  (let ((__function__ '4vec-parity))
    (declare (ignorable __function__))
    (if (and (2vec-p x) (<= 0 (2vec->val x)))
        (b* ((x (2vec->val x)))
          (2vec (- (fast-parity (+ 1 (integer-length x))
                                x))))
      (4vec-x))))

Theorem: 3vec-p!-of-4vec-parity

(defthm 3vec-p!-of-4vec-parity
  (b* ((parity (4vec-parity x)))
    (3vec-p! parity))
  :rule-classes :rewrite)

Theorem: 4vec-parity-of-2vecx-fix-x

(defthm 4vec-parity-of-2vecx-fix-x
  (equal (4vec-parity (2vecx-fix x))
         (4vec-parity x)))

Theorem: 4vec-parity-2vecx-equiv-congruence-on-x

(defthm 4vec-parity-2vecx-equiv-congruence-on-x
  (implies (2vecx-equiv x x-equiv)
           (equal (4vec-parity x)
                  (4vec-parity x-equiv)))
  :rule-classes :congruence)