• 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

4v-operations

Primitive operations in our four-valued logic.

This is a collection of operations on 4vps that are generally meant to model the behavior of particular, primitive kinds of circuits. For instance, in the esim hardware simulator, the esim-primitives are generally based on these operations.

The operations here apply to four-valued constants and produce new four-valued constants as results. If you are looking for operations that construct new 4v-sexprs, see instead the 4vs-constructors.

Note that all of these operations are monotonic.

Subtopics

4v-ite
Less-conservative four-valued semantics for a multiplexor (mux).
4v-res
Four-valued semantics for connecting multiple wires together.
4v-not-list
(4v-not-list x) maps 4v-not across a list.
4v-unfloat
Converts floating (undriven) values to X.
4v-wand
Four-valued semantics for a wired and.
4v-wor
Four-valued semantics for a wired or.
4v-zif
Unusual semantics for a multiplexor, used mainly to implement composition features in esim
4v-tristate
Four-valued semantics for tri-state buffers.
4v-xdet
X-detection or identity circuit.
4v-xor
Four-valued semantics for xor gates.
4v-iff
Four-valued semantics for xnor gates.
4v-and
Four-valued semantics for and gates.
4v-or
Four-valued semantics for or gates.
4v-not
Four-valued semantics for not gates.
4v-pullup
Four-valued semantics for a pullup resistor.
4v-and-list
(4v-and-list x) conjoins a list of 4vp constants.
4v-ite*
More-conservative four-valued semantics for a multiplexor.