• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
      • 4v-monotonicity
      • 4v-operations
        • 4v-ite
        • 4v-res
        • 4v-not-list
        • 4v-unfloat
        • 4v-wand
        • 4v-wor
        • 4v-tristate
        • 4v-zif
        • 4v-xdet
        • 4v-xor
        • 4v-iff
        • 4v-and
        • 4v-or
        • 4v-not
        • 4v-pullup
        • 4v-and-list
        • 4v-ite*
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-operations

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))