If-then-elses of s4vecs following the SystemVerilog semantics for procedural conditional branches, i.e. if the test has any bit that is exactly 1 (not 0, Z, or X), we choose the then branch, else the else branch. (Non-monotonic semantics).
Function:
(defun s4vec-?! (test then else) (declare (xargs :guard (and (s4vec-p test) (s4vec-p then) (s4vec-p else)))) (let ((__function__ 's4vec-?!)) (declare (ignorable __function__)) (b* (((s4vec test)) (pick-else (sparseint-equal 0 (sparseint-bitand test.upper test.lower)))) (if pick-else (s4vec-fix else) (s4vec-fix then)))))
Theorem:
(defthm s4vec-p-of-s4vec-?! (b* ((choices (s4vec-?! test then else))) (s4vec-p choices)) :rule-classes :rewrite)
Theorem:
(defthm s4vec-?!-correct (b* ((?choices (s4vec-?! test then else))) (equal (s4vec->4vec choices) (4vec-?! (s4vec->4vec test) (s4vec->4vec then) (s4vec->4vec else)))))
Theorem:
(defthm s4vec-?!-of-s4vec-fix-test (equal (s4vec-?! (s4vec-fix test) then else) (s4vec-?! test then else)))
Theorem:
(defthm s4vec-?!-s4vec-equiv-congruence-on-test (implies (s4vec-equiv test test-equiv) (equal (s4vec-?! test then else) (s4vec-?! test-equiv then else))) :rule-classes :congruence)
Theorem:
(defthm s4vec-?!-of-s4vec-fix-then (equal (s4vec-?! test (s4vec-fix then) else) (s4vec-?! test then else)))
Theorem:
(defthm s4vec-?!-s4vec-equiv-congruence-on-then (implies (s4vec-equiv then then-equiv) (equal (s4vec-?! test then else) (s4vec-?! test then-equiv else))) :rule-classes :congruence)
Theorem:
(defthm s4vec-?!-of-s4vec-fix-else (equal (s4vec-?! test then (s4vec-fix else)) (s4vec-?! test then else)))
Theorem:
(defthm s4vec-?!-s4vec-equiv-congruence-on-else (implies (s4vec-equiv else else-equiv) (equal (s4vec-?! test then else) (s4vec-?! test then else-equiv))) :rule-classes :congruence)