Faig-constructors
Low-level functions for constructing faigs.
These functions construct new FAIGs from existing ones. They
typically honsing up some new onset and offset aigs by using the
using aig-constructors like aig-and and aig-not, and then
cons those new onset/offset AIGs together to form a new FAIG.
Most of these functions are geared toward modeling hardware. For instance,
f-aig-and is intended to produce a new FAIG that captures the
four-valued logic semantics of an AND gate.
Note: the details about how X and Z are handled by these functions are
often subtle and this documentation doesn't really explain why these
functions work the way they do. However, for most functions here there
are corresponding 4v-operations, and the documentation there typically
does explaining the X/Z behavior.
Three-valued (T-) vs. Four-valued (F-) constructors
There is an important optimization you can make when modeling hardware gates
as FAIGs. In particular, it is often possible to construct more
efficient (smaller) FAIGs to represent the gate's output when you know that the
gate's inputs cannot evaluate to Z.
In CMOS designs, this property—never evaluating to Z—holds for
the outputs of most logic gates. Accordingly, it's true for most inputs
to other gates. For example, suppose you are trying to model a circuit like
this:
|\ b
---| >o---+
|/ | ____
+------| \
| | and )---
---| >o----------|____/ o
|/ a
Here, we know that wires a and b can never have the value Z,
because they are produced by NOT gates. Accordingly, when we want to create
the FAIG corresponding to o, we can use an optimized, less-general
implementation of the and gate, where we assume that our inputs are
non-Z.
Of course, some logic gates (e.g., tri-state buffers) can produce Z
valued outputs, so occasionally these sorts of optimizations aren't possible.
Because of this, we typically have two versions of each FAIG constructor:
- t-aig-* functions make the assumption that their inputs can never
evaluate to Z. These are generally more efficient, and will produce smaller
AIGs that are easier to analyze with SAT solvers.
- f-aig-* functions do not make this assumption. This makes them more
general purpose and able to operate on any FAIG inputs, at the cost of larger
AIGs.
Rulesets
For historic reasons these functions are left enabled. There are two
useful rulesets you can use to disable them:
- f-aig-defs has all of the f- constructors.
- t-aig-defs has all of the t- constructors.
Subtopics
- T-aig-ite*
- (t-aig-ite* c a b) constructs a (more conservative) FAIG representing
(if c a b), assuming these input FAIGs cannot evaluate to Z.
- F-aig-ite*
- (f-aig-ite* c a b) constructs a (more conservative) FAIG representing
(if c a b), assuming these input FAIGs cannot evaluate to Z.
- T-aig-ite
- (t-aig-ite c a b) constructs a (less conservative) FAIG representing
(if c a b), assuming these input FAIGs cannot evaluate to Z.
- F-aig-ite
- (f-aig-ite c a b) constructs a (less conservative) FAIG representing
(if c a b).
- T-aig-tristate
- (t-aig-tristate c a) constructs an FAIG representing a tri-state
buffer whose inputs are known to be non-X.
- F-aig-zif
- (f-aig-zif c a b) constructs an FAIG representing a kind of pass gate
style mux.
- T-aig-xor
- (t-aig-xor a b) xors together the FAIGs a and b,
assuming they cannot evaluate to Z.
- T-aig-or
- (t-aig-or a b) ors together the FAIGs a and b,
assuming they cannot evaluate to Z.
- T-aig-iff
- (t-aig-iff a b) iffs together the FAIGs a and b,
assuming they cannot evaluate to Z.
- T-aig-and
- (t-aig-and a b) ands together the FAIGs a and b,
assuming they cannot evaluate to Z.
- F-aig-and
- (f-aig-and a b) ands together the FAIGs a and b.
- F-aig-xor
- (f-aig-xor a b) xors together the FAIGs a and b.
- F-aig-or
- (f-aig-or a b) ors together the FAIGs a and b.
- F-aig-iff
- (f-aig-iff a b) iffs together the FAIGs a and b.
- F-aig-res
- (f-aig-res x y) constructs a FAIG that represents the result of
connecting two (independently driven) wires together.
- F-aig-unfloat
- (f-aig-unfloat a) converts floating (Z) values to unknown (X)
values.
- T-aig-not
- (t-aig-not a) negates the FAIG a, assuming that it cannot
evaluate to Z.
- F-aig-pullup
- (f-aig-pullup a) constructs an FAIG representing a pullup
resistor.
- F-aig-not
- (f-aig-not a) negates the FAIG a.
- T-aig-xdet
- (t-aig-xdet a) constructs an FAIG for 4v-xdet, assuming
that the argument a cannot evaluate to Z.
- F-aig-xdet
- (f-aig-xdet a) constructs an FAIG for 4v-xdet.