		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-reduction-and

Reduction logical AND of a 4vec.

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

ANDs together all of the bits in a 4vec. Following the boolean-convention, we return:

True (all 1s) if all of the (infinite) bits are 1, i.e., if X is -1,
False (all 0s) if there is any bit that is 0, or
All Xes otherwise.

Subtle. Since 4vecs are ``infinite width,'' reduction operations are a bit unusual. For reduction AND in particular, when translating from Verilog or other languages where your vectors are only some fixed width, you will typically need to always sign-extend the input vector, regardless of whether it is signed or unsigned.

That is, say you start with a unsigned 5-bit vector whose value is 11111. If you create your (infinite width) 4vec for this by zero extension, you'll end up with infinitely many leading 0s, which will cause the reduction AND of your vector to be 0!

Definitions and Theorems

Function: 4vec-reduction-and

(defun 4vec-reduction-and (x)
  (declare (xargs :guard (4vec-p x)))
  (let ((__function__ '4vec-reduction-and))
    (declare (ignorable __function__))
    (3vec-reduction-and (3vec-fix x))))

Theorem: 3vec-p!-of-4vec-reduction-and

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

Theorem: 4vec-reduction-and-recursive

(defthm 4vec-reduction-and-recursive
 (equal
  (4vec-reduction-and x)
  (b*
   (((4vec x))
    ((when (and (or (zip x.upper) (eql x.upper -1))
                (or (zip x.lower) (eql x.lower -1))))
     (3vec-fix x))
    (first (4vec-idx->4v 0 x))
    (and-rest
       (4vec-idx->4v 0
                     (4vec-reduction-and (4vec (logcdr x.upper)
                                               (logcdr x.lower))))))
   (4v->4vec-bit (acl2::4v-and first and-rest))))
 :rule-classes
 ((:definition :install-body nil
               :clique (4vec-reduction-and)
               :controller-alist ((4vec-reduction-and t)))))

Theorem: 4vec-reduction-and-of-3vec-fix-x

(defthm 4vec-reduction-and-of-3vec-fix-x
  (equal (4vec-reduction-and (3vec-fix x))
         (4vec-reduction-and x)))

Theorem: 4vec-reduction-and-3vec-equiv-congruence-on-x

(defthm 4vec-reduction-and-3vec-equiv-congruence-on-x
  (implies (3vec-equiv x x-equiv)
           (equal (4vec-reduction-and x)
                  (4vec-reduction-and x-equiv)))
  :rule-classes :congruence)