• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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-zif
        • 4v-tristate
        • 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
  • Testing-utilities
  • Math

• 4v-operations

4v-wand

Four-valued semantics for a wired and.

(4v-wand a b) returns:

• F when either input is F, or
• Z when both inputs are Z, or
• T when one input is T and the other is T/Z, or
• X otherwise.

We use this to model what happens when multiple signals are connected in a wired and arrangement.

The full truth table is shown below. It intentionally corresponds to the Verilog semantics for wired ors (Section 4.6.2 of the Verilog 2005 specification).

     |   F   T   X   Z  |
-----+------------------+
  F  |   F   F   F   F  |
  T  |   F   T   X   T  |
  X  |   F   X   X   X  |
  Z  |   F   T   X   Z  |
-----+------------------+

Definitions and Theorems

Function: 4v-wand

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

Theorem: 4v-wand-truth-table

(defthm 4v-wand-truth-table
        (and (equal (4v-wand (4vf) (4vf)) (4vf))
             (equal (4v-wand (4vf) (4vt)) (4vf))
             (equal (4v-wand (4vf) (4vx)) (4vf))
             (equal (4v-wand (4vf) (4vz)) (4vf))
             (equal (4v-wand (4vt) (4vf)) (4vf))
             (equal (4v-wand (4vt) (4vt)) (4vt))
             (equal (4v-wand (4vt) (4vx)) (4vx))
             (equal (4v-wand (4vt) (4vz)) (4vt))
             (equal (4v-wand (4vx) (4vf)) (4vf))
             (equal (4v-wand (4vx) (4vt)) (4vx))
             (equal (4v-wand (4vx) (4vx)) (4vx))
             (equal (4v-wand (4vx) (4vz)) (4vx))
             (equal (4v-wand (4vz) (4vf)) (4vf))
             (equal (4v-wand (4vz) (4vt)) (4vt))
             (equal (4v-wand (4vz) (4vx)) (4vx))
             (equal (4v-wand (4vz) (4vz)) (4vz)))
        :rule-classes nil)

Theorem: 4v-equiv-implies-equal-4v-wand-2

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

Theorem: 4v-equiv-implies-equal-4v-wand-1

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