• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
      • 4v
        • 4v-sexprs
        • 4v-monotonicity
        • 4v-operations
        • Why-4v-logic
          • 4v-<=
          • 4vp
          • 4vcases
          • 4v-fix
          • 4v-lookup
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • 4v

    Why-4v-logic

    Motivation for using a four-valued logic.

    Why use a four-valued logic instead of a simple, two-valued, Boolean logic with just T and F?

    Having an X value is fundamental to the semantics of esim, our circuit evaluator. Loosely speaking, when we begin simulating a circuit, all of the internal wires are given X as their value. We then evaluate all of the submodule occurrences. Because of monotonicity, these evaluations can only change wires from X to a different value. This puts a bound on the maximum number of evaluation steps required for the circuit's wires to reach a fixed point.

    In the context of symbolic simulation, X values are sometimes also useful as a way to ignore certain signals. For instance, if we think some inputs to a particular circuit are not even involved in the property we wish to prove, we may leave them as X.

    X values also allow us to model some circuits which cannot be expressed with just Boolean logic. For instance, imagine a scenario like:

          Diagram                      Verilog
           ____
          |    \                    assign C = ~A;
    A  ---|     o------+            assign C = ~B;
          |____/       |
           ____        |-- C
          |    \       |
    B  ---|     o------+
          |____/

    Here the wire C is being driven by two separate sources. When these sources have different values, e.g., suppose A is T and B is F, then C is simultaneously driven to both F and T. We do not know which value will "win," or, really, whether there will even be a winner. So in this case we just say the value of C is X. Without an X value, we would not be able to model this circuit.

    The Z value allows us to model additional circuits, even beyond those circuits that are possible to model using Xes. In the circuit above, we did not need a Z value because not-gates always drive at least some value onto C. But other kinds of circuits do not necessarily drive their output. For instance, in Verilog one might describe a mux whose selects must be one-hot as follows:

    assign C = S1 ? A : 1'bz;
    assign C = S2 ? B : 1'bz;
    ...

    By adopting Z into our logic, we can model these kinds of assignments directly, e.g., see 4v-tristate and 4v-res.