		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-?

Atomic if-then-else of 4vecs; doesn't unfloat then/else values.

Signature
(4vec-? test then else) → choice
Arguments: test — Guard (4vec-p test).; then — Guard (4vec-p then).; else — Guard (4vec-p else).
Returns: choice — Type (4vec-p choice).

Easy cases: when test has any 1-bits we return then; when test is 0 we return else.

Note that the behavior in these cases is not very conservative. In particular, the then and else branches are passed through without ``unfloating'' Z values. This agrees with the Verilog and SystemVerilog semantics for the ?: operators, but it does not agree with how some mux implementations behave in hardware, e.g., and/or style muxes.

Hard case: when test has some X or Z bits, we merge the bits of then and else, setting each bit of the result to:

Xes in bit positions where then and else are unequal or both Z, or
The agreed upon Boolean value, otherwise.

Definitions and Theorems

Function: 4vec-?

(defun 4vec-? (test then else)
  (declare (xargs :guard (and (4vec-p test)
                              (4vec-p then)
                              (4vec-p else))))
  (let ((__function__ '4vec-?))
    (declare (ignorable __function__))
    (3vec-? (3vec-fix test) then else)))

Theorem: 4vec-p-of-4vec-?

(defthm 4vec-p-of-4vec-?
  (b* ((choice (4vec-? test then else)))
    (4vec-p choice))
  :rule-classes :rewrite)

Theorem: 4vec-?-of-3vec-fix-test

(defthm 4vec-?-of-3vec-fix-test
  (equal (4vec-? (3vec-fix test) then else)
         (4vec-? test then else)))

Theorem: 4vec-?-3vec-equiv-congruence-on-test

(defthm 4vec-?-3vec-equiv-congruence-on-test
  (implies (3vec-equiv test test-equiv)
           (equal (4vec-? test then else)
                  (4vec-? test-equiv then else)))
  :rule-classes :congruence)

Theorem: 4vec-?-of-4vec-fix-then

(defthm 4vec-?-of-4vec-fix-then
  (equal (4vec-? test (4vec-fix then) else)
         (4vec-? test then else)))

Theorem: 4vec-?-4vec-equiv-congruence-on-then

(defthm 4vec-?-4vec-equiv-congruence-on-then
  (implies (4vec-equiv then then-equiv)
           (equal (4vec-? test then else)
                  (4vec-? test then-equiv else)))
  :rule-classes :congruence)

Theorem: 4vec-?-of-4vec-fix-else

(defthm 4vec-?-of-4vec-fix-else
  (equal (4vec-? test then (4vec-fix else))
         (4vec-? test then else)))

Theorem: 4vec-?-4vec-equiv-congruence-on-else

(defthm 4vec-?-4vec-equiv-congruence-on-else
  (implies (4vec-equiv else else-equiv)
           (equal (4vec-? test then else)
                  (4vec-? test then else-equiv)))
  :rule-classes :congruence)