		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-res

Bitwise wire resolution of two 4vecs.

Signature
(4vec-res a b) → ans
Arguments: a — Guard (4vec-p a).; b — Guard (4vec-p b).
Returns: ans — Type (4vec-p ans).

Resolves together two 4vecs as if they were both shorted together. Each bit of the result is determined by the corresponding bits of the two inputs as follows:

If both input bits have the same value, then the resulting bit is that value.
If one input bit is Z, the result is the other input bit.
Otherwise, the result is X.

Definitions and Theorems

Function: 4vec-res

(defun 4vec-res (a b)
  (declare (xargs :guard (and (4vec-p a) (4vec-p b))))
  (let ((__function__ '4vec-res))
    (declare (ignorable __function__))
    (b* (((4vec a)) ((4vec b)))
      (4vec (logior a.upper b.upper)
            (logand a.lower b.lower)))))

Theorem: 4vec-p-of-4vec-res

(defthm 4vec-p-of-4vec-res
  (b* ((ans (4vec-res a b))) (4vec-p ans))
  :rule-classes :rewrite)

Main correctness theorem: each result bit is just the ACL2::4v-res of the corresponding input bits.

Theorem: 4vec-res-bits

(defthm 4vec-res-bits
  (equal (4vec-idx->4v n (4vec-res x y))
         (acl2::4v-res (4vec-idx->4v n x)
                       (4vec-idx->4v n y))))

Theorem: 4vec-res-of-4vec-fix-a

(defthm 4vec-res-of-4vec-fix-a
  (equal (4vec-res (4vec-fix a) b)
         (4vec-res a b)))

Theorem: 4vec-res-4vec-equiv-congruence-on-a

(defthm 4vec-res-4vec-equiv-congruence-on-a
  (implies (4vec-equiv a a-equiv)
           (equal (4vec-res a b)
                  (4vec-res a-equiv b)))
  :rule-classes :congruence)

Theorem: 4vec-res-of-4vec-fix-b

(defthm 4vec-res-of-4vec-fix-b
  (equal (4vec-res a (4vec-fix b))
         (4vec-res a b)))

Theorem: 4vec-res-4vec-equiv-congruence-on-b

(defthm 4vec-res-4vec-equiv-congruence-on-b
  (implies (4vec-equiv b b-equiv)
           (equal (4vec-res a b)
                  (4vec-res a b-equiv)))
  :rule-classes :congruence)