4v
An hons-based, s-expression representation of monotonic, four-valued functions.
This library defines the logic of the esim symbolic
simulator. By "four-valued", we mean that each wire can take one of the four
values recognized by 4vp:
- X represents "unknown" values
- Z represents an "undriven" or "floating" value
- T represents logical truth
- F represents logical falsity
The non-Boolean values X and Z are often
useful when modeling hardware, and are intended to correspond to
Verilog's notions of X and Z.
Our logic has a fixed set of primitive 4v-operations that model, for
instance, how an AND gate behaves when given a pair of four-valued inputs. On
top of these primitives, we use a simplified s-expression syntax to represent expressions in the logic.
The semantics of these s-expressions are defined by 4v-sexpr-eval, a
simple evaluator that can look up variables and apply the primitive
operations.
A feature of our logic is that all the primitives are intrinsically monotonic, which loosely means that they
properly treat X inputs as unknowns. The monotonicity of the primitives
carries over to the s-expressions.
Subtopics
- 4v-sexprs
- S-Expression representation of four-valued expressions.
- 4v-monotonicity
- The monotonicity property satisfied by all 4v-operations.
- 4v-operations
- Primitive operations in our four-valued logic.
- Why-4v-logic
- Motivation for using a four-valued logic.
- 4v-<=
- Four-valued lattice-ordering comparison.
- 4vp
- Recognizer for four-valued logic constants.
- 4vcases
- Macro for cases on the 4-valued logic constants.
- 4v-fix
- Fixing function for four-valued constants.
- 4v-lookup
- Alist lookup that automatically 4v-fixes its result.
