Faig
A hons-based representation of four-valued functions as
pairs of aigs.
A FAIG (Four-valued AIG) combines two aigs together
to represent a function with four possible values. Such functions can be
useful in hardware verification.
We represent an FAIG as the cons of two AIGs, which are called the
onset and offset of the FAIG. Our FAIG evaluation function,
faig-eval, just evaluates these two AIGs, separately, using ordinary
aig-eval, and conses together the resulting Boolean values. So, the
four possible values of an FAIG are:
- (nil . nil), which we call Z,
- (t . nil), which we call True,
- (nil . t), which we call False, and
- (t . t), which we call X.
We generally think of the onset as being a Boolean functions that should
evaluate to T when the wire is being driven to 1. The offset is similar,
but indicates whether the wire is being driven to 0. So, the Z value
represents a situation where the wire is completely undriven, and the X value
represents a bad case where the wire is simultaneously driven to both True and
False.
Hons convention. We ordinarly construct all AIGs with hons, but we
don't bother to hons the FAIG conses that put these AIGs together.
Subtopics
- Faig-constructors
- Low-level functions for constructing faigs.
- Faig-onoff-equiv
- We say the objects X and Y are equivalent if they are (1)
faig-equiv, and (2) both atoms or both conses.
- Faig-purebool-p
- Does a FAIG always evaluate to a purely Boolean value, i.e., is it
never X or Z?
- Faig-alist-equiv
- We say the FAIG Alists X and Y are equivalent when they
bind the same keys to equivalent FAIGs, in the sense of faig-equiv.
- Faig-equiv
- We say the FAIGs X and Y are equivalent when they always
evaluate to the same value, per faig-eval.
- Faig-eval
- (faig-eval x env) evaluates x, a faig, under the
environment env, producing a pair of Boolean values.
- Faig-restrict
- (faig-restrict x sigma) performs variable substitution throughout the
FAIG x, replacing any variables bound in sigma with their
corresponding values.
- Faig-fix
- (faig-fix x) is the identity for FAIGs, but coerces atoms to
(t . t), i.e., X.
- Faig-partial-eval
- (faig-partial-eval x env) evaluates x, an FAIG, under the
partial environment env, producing a new FAIG as a result.
- Faig-compose
- (faig-compose x sigma) performs variable substitution throughout the
FAIG x, unconditionally replacing every variable in x with its
binding in sigma.
- Faig-compose-alist
- (faig-compose-alist x sigma) composes into an FAIG Alist (an alist
binding keys to FAIGs).
- Patbind-faig
- b* binder that binds two variables to the onset and offset,
respectively, of the faig-fix of the given expression.
- Faig-constants
- The four faig values, representing true, false, X, and Z.
