2000 | OriginalPaper | Buchkapitel
Building Circuits from Relations
verfasst von : James H. Kukula, Thomas R. Shiple
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Given a Free BDD for the characteristic function of an input-output relation T(x, y), we show how to construct a combinational logic circuit satisfying that relation. Such relations occur as environmental constraints for module specifications, as parts of a proof strategies, or can be computed from existing circuits, e.g., by formal analysis of combinational cycles. The resulting circuit C can be used for further analysis, e.g. symbolic simulation, or to reformat a circuit as a logic optimization tactic.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.