# 4v-res

Four-valued semantics for connecting multiple wires together.

`(4v-res a b)` is a funny kind of operation that resolves what
happens when multiple signals are wired together.

Suppose we have the following circuit:

.------------. A ...
| some cloud |-----+ |
| of logic | | ___|
'------------' |_____||
| ||___
.------------. | |
| some cloud |-----+ |
| of logic | B ...
'------------'

Because esim does support driving a single wire with multiple
sources, we model such a circuit by inserting a "resolution" module:

.------------. A ...
| some cloud |-----+ |
| of logic | | ___|
'------------' +-----+ ||
| res |---C ---||
+-----+ ||___
.------------. | |
| some cloud |-----+ |
| of logic | B ...
'------------'

`(4v-res a b)` produces the value for C as follows:

- The shared value of A and B when they agree, or
- The value on the other wire, when one of A or B is Z, or
- X otherwise.

This is, of course, not a full model of transistor-level behavior. It does
not account for the possibility that values could flow "backwards" from the
the circuitry connected to C, so it is only appropriate for cases where C is
really being used to gate a transistor.

It also does not account for the possibility that values could flow
"between" the clouds of logic producing A and B. If, say, A and B are gate
outputs that are being driven to different values, then wiring them together
produces a short circuit!

### Definitions and Theorems

**Function: **4v-res

(defun 4v-res (a b)
(declare (xargs :guard t))
(mbe :logic
(4vcases a (z (4v-fix b))
(& (4vcases b (z (4v-fix a))
(& (let ((a (4v-fix a)) (b (4v-fix b)))
(if (eq a b) a (4vx)))))))
:exec (cond ((eq a (4vz))
(if (or (eq b (4vt))
(eq b (4vf))
(eq b (4vz)))
b
(4vx)))
((eq b (4vz))
(if (or (eq a (4vt)) (eq a (4vf)))
a
(4vx)))
(t (if (and (or (eq a (4vt)) (eq a (4vf)))
(eq a b))
a
(4vx))))))

**Theorem: **4v-equiv-implies-equal-4v-res-2

(defthm 4v-equiv-implies-equal-4v-res-2
(implies (4v-equiv b b-equiv)
(equal (4v-res a b) (4v-res a b-equiv)))
:rule-classes (:congruence))

**Theorem: **4v-equiv-implies-equal-4v-res-1

(defthm 4v-equiv-implies-equal-4v-res-1
(implies (4v-equiv a a-equiv)
(equal (4v-res a b) (4v-res a-equiv b)))
:rule-classes (:congruence))