Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Aagaard, M., Jones, R., Seger, C.-J.: FormalVerification Using Parametric Representation of Boolean Constraints. In: Proc. of the Design Automation Conf., June 1999, pp. 402–407 (1999)
Ashar, P., Devadas, S., Keutzer, K.: Gate-delay-fault Testability Properties of Multiplexor- Based Networks. Formal Methods in System Design 1, 93–112 (1993)
Bertacco, V., Damiani, M., Quer, S.: Cycle-based Symbolic Simulation of Gate-level Synchronous Circuits. In: Proc. of the Design Automation Conf., June 1999, pp. 391–396 (1999)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. Tools and Algorithms for the Analysis and Construction of Systems (1999)
Boppana, V., Rajan, S., Takayama, K., Fujita, M.: Model Checking Based on Sequential ATPG. In: Proc. of the Computer Aided Verification Conf., July 1999, pp. 418–430 (1999)
Brace, K., Rudell, R., Bryant, R.: Efficient Implementation of a BDD Package. In: Proc. of the Design Automation Conf., June 1990, pp. 40–45 (1990)
Brown, F.M.: Boolean Reasoning. Kluwer, Dordrecht (1990)
Bryant, R.: Graph BasedAlgorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35, 677–691 (1986)
Gergov, J., Meinel, C.: Efficient Boolean Manipulation with OBDD’s Can Be Extended to FBDD’s. IEEE Transactions on Computers 43, 1197–1209 (1994)
Günther, W., Dreschler, R.: Minimization of Free BDDs. In: Proc. Asia and South Pacific Design Automation Conference (January 1999)
Ishiura, N., Sawada, H., Yajima, S.: Minimization of Binary Decision Diagrams Based on Exchanges ofVariables. In: Proc. Intl. Conf. on Computer-Aided Design, pp. 472–475 (November 1991)
Jain, P., Gopalakrishnan, G.: Efficient Symbolic Simulation-Based Verification Using the Parametric Form of Boolean Expressions. IEEE Transactions on Computer-Aided Design 13, 1005–1015 (1994)
Kukula, J., Shiple, T., Aziz, A.: Techniques for Implicit State Enumeration of EFSMs. In: Proc. of the Formal Methods in CAD Conf., November 1998, pp. 469–482 (1998)
McMillan, K.: Symbolic Model Checking. Kluwer, Dordrecht (1993)
Namjoshi, K., Kurshan, R.: Efficient Analysis of Cyclic Definitions. In: Proc. of the Computer Aided Verification Conf., July 1999, pp. 394–405 (1999)
Rudell, R.: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. In: Proc. Intl. Conf. on Computer-Aided Design, November 1993, pp. 42–47 (1993)
Shiple, T.: Formal Analysis of Synchronous Circuits. PhD Diss., Univ. Calif. Berkeley (1996)
Watanabe, Y., Guerra, L., Brayton, R.: Permissible Functions for Multioutput Components in Combinational Logic Optimization. IEEE Transactions on Computer-Aided Design 15, 732–744 (1996)
Yuan, J., Shultz, K., Pixley, C., Miller, H., Aziz, A.: Modeling Design Constraints and Biasing in Simulation Using BDDs. In: Proc. Intl. Conf. on Computer-Aided Design, Novemeber 1999, pp. 584–589 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kukula, J.H., Shiple, T.R. (2000). Building Circuits from Relations. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_12
Download citation
DOI: https://doi.org/10.1007/10722167_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive