| |
|
|
Building Circuits from RelationsAbstractGiven a BDD for the characteristic function of an input-output relation T, we show how to construct a combinational logic circuit satisfying that relation. Such relations occur as environmental constraints for module specifications, as parts of proof strategies, or can be computed from existing circuits, for example, by formal analysis of combinational cycles. The resulting circuit C can be used for further analysis, for example, symbolic simulation or logic emulation.The constructed circuit includes supplementary parametric inputs to allow all legal outputs to be generated in the case that T is non-deterministic. The structure of the circuit is isomorphic to that of the BDD for T, and hence is as compact as the BDD. In particular, when T represents a relation between bit vector integer values definable in Presburger arithmetic, the constructed circuit will have a regular bit slice form.
This is joint work with Jim Kukula.
|