This Article 
 Bibliographic References 
 Add to: 
Formal Verification Using Edge-Valued Binary Decision Diagrams
February 1996 (vol. 45 no. 2)
pp. 247-255

Abstract-In this paper we present a new data structure called Edge-Valued Binary-Decision Diagrams (EVBDD). An EVBDD is a directed acyclic graph, that provides a canonical and compact representation of functions that involve both Boolean and integer quantities. In general, EVBDDs provide a more versatile and powerful representation than Ordinary Binary Decision Diagrams. We first describe the structure and properties of EVBDDs, and present a general algorithm for performing a variety of binary operations. Next, we describe an important extension of EVBDDs, called StructuralEVBDDs, and show how they can be used for hierarchical verification.

[1] G.V. Bochmann, "Hardware specification with temporal logic: An example," IEEE Trans. Computers, vol. 31, no. 3, pp. 223-231, Mar. 1982.
[2] R.T. Boute, "Representational and denotational semantics of digital systems," IEEE Trans. Computers, vol. 38, no. 7, pp. 986-999, July 1989.
[3] K.S. Brace, R.L. Rudell, and R.E. Bryant, Efficient Implementation of a BDD Package Proc. Design Automation Conf., pp. 40-45, 1990.
[4] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[5] R.E. Bryant, D. Beatty, K. Brace, K. Cho, and T. Sheffler, "COSMOS: A Compiled Simulator for MOS Circuits," Proc. Design Automation Conf., pp. 9-16. ACM/IEEE, June 1987.
[6] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293-318, 1992.
[7] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[8] E.M. Clarke, M. Fujita, P.C. McGeer, K.L. McMillan, and J.C.-Y. Yang, "Multi-terminal binary decision diagrams: An efficient data structure for matrix representation," Int'l Workshop Logic Synthesis, pp. 6a:1-15, May 1993.
[9] E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang, "Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping," Proc. 30th Design Automation Conf., pp. 54-60, 1993.
[10] O. Coudert, C. Berthet, and J.C. Madre, “Verification of Sequential Machines Based on Symbolic Execution,” Proc. Workshop Automatic Verification Methods for Finite State Systems, 1989.
[11] M.J.C. Gordon, "Why higher-order logic is a good formalism for specifying and verifying hardware," Formal Aspects of VLSI Designs, G.J. Milne and P.A. Subrahmanyam, eds., pp. 153-177, 1986.
[12] P.L. Hammer and S. Rudeanu, Boolean Methods in Operations Research and Related Areas.Heidelberg: Springer-Verlag, 1968.
[13] Y-T. Lai and S. Sastry (S.B.K. Vrudhula), "Edge-valued binary decision diagrams for multi-level hierarchical verification," Proc. 29th Design Automation Conf., pp. 608-613, 1992.
[14] R.J. Bayardo, “Efficiently Mining Long Patterns From Databases,” ACM SIGMOD Conf. Management of Data, June 1998.
[15] Y-T. Lai, M. Pedram, and S. Sastry (S.B.K. Vrudhula), "BDD based decomposition of logic functions with application to FPGA synthesis," Proc. 30th Design Automation Conf, pp. 642-647, 1993.
[16] Y-T. Lai, M. Pedram, and S. Sastry (S.B.K. Vrudhula), "FGILP: An integer linear program solver based on function graphs," Proc. Int'l Conf. Computer Aided Design, 1993.
[17] Y-T. Lai,, "Logic verification and synthesis using function graphs," PhD dissertation, Computer Eng., Univ. of Southern California, Dec. 1993.
[18] Y.T. Lai, M. Pedram, and S.B.K. Vrudhula, “EVBDD-Based Algorithms for Integer Linear Programming, Spectral Transformation, and Functional Decomposition,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 13, no. 8, pp. 959-975, Aug. 1994.
[19] H-T. Liaw and C-S Lin, "On the OBDD-representation of general Boolean functions," IEEE Trans. Computers, vol. 41, no. 6, pp. 661-664, June 1992.
[20] G.J. Milne, "CIRCAL and the representation of communication, concurrency, and time," ACM Trans. Programming Languages and Systems, vol. 7, no. 2, pp. 270-298, Apr. 1985.
[21] A. Srinivasan, T. Kam, S. Malik, and R.E. Brayton, Algorithms for Discrete Function Manipulation Proc. Int'l Conf. CAD (ICCAD '90), pp. 92-95, 1990.
[22] Texas Instruments, "The TTL data book for design engineers," Texas Instruments, 1984.

Index Terms:
Binary decision diagrams, Boolean functions, pseudo-Boolean functions, verification,
Yung-Te Lai, Massoud Pedram, Sarma B.K. Vrudhula, "Formal Verification Using Edge-Valued Binary Decision Diagrams," IEEE Transactions on Computers, vol. 45, no. 2, pp. 247-255, Feb. 1996, doi:10.1109/12.485378
Usage of this product signifies your acceptance of the Terms of Use.