		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-resor

Bitwise wired OR resolution of two 4vecs.

Signature
(4vec-resor 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 assigned to a wor net in Verilog. Each bit of the result is determined by the corresponding bits of the two inputs as follows:

If either input is 1, the result is 1.
If either input is Z, the result is the other input bit.
If both inputs are 0, the result is 0.
If one input is X and the other is not 1, the result is X.

Definitions and Theorems

Function: 4vec-resor

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

Theorem: 4vec-p-of-4vec-resor

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

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

Theorem: 4vec-resor-bits

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

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

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

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

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

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

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

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

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