Aignet-transforms
Various types of transforms preserving different properties of the AIG
The following kinds of transforms are defined:
Each of these transform types has a constrained function,
apply-<name>-transform, which takes a source AIG aignet, a
destination AIG aignet2, a configuration object, and the ACL2 state and
returns a modified destination AIG and state. The constraints on these define
the contracts of each transform type. Using this stub function, we also define
apply-<name>-transform! which uses swap-stobjs to overwrite the
source AIG with the result instead of dealing with a second destination AIG.
The properties defining these transforms are all transitive, so for each type
we also define functions apply-<name>-transforms and
apply-<name>-transforms! which apply a sequence of transforms specified by
a list of configuration objects.
Each of the transform types has an implementation of its constrained
apply function defined in centaur/aignet/transforms.lisp and
attached to the apply function when that book is included.
Subtopics
- Aignet-output-ranges
- Summary of a system to specify the treatments of different primary outputs by AIG transformations
- Aignet-comb-transforms
- Aignet transforms that simplify the network while preserving combinational equivalence
- Aignet-m-assumption-n-output-transforms
- Aignet transforms that simplify the network while preserving combinational
equivalence of the first M primary outputs and combinational equivalence
when assuming the first M primary outputs true on the next N primary
outputs.
- Aignet-n-output-comb-transforms
- Aignet transforms that simplify the network while preserving combinational
equivalence of the first N primary outputs.
