
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
YungTe Lai, Massoud Pedram, Sarma B.K. Vrudhula, "Formal Verification Using EdgeValued Binary Decision Diagrams," IEEE Transactions on Computers, vol. 45, no. 2, pp. 247255, February, 1996.  
BibTex  x  
@article{ 10.1109/12.485378, author = {YungTe Lai and Massoud Pedram and Sarma B.K. Vrudhula}, title = {Formal Verification Using EdgeValued Binary Decision Diagrams}, journal ={IEEE Transactions on Computers}, volume = {45}, number = {2}, issn = {00189340}, year = {1996}, pages = {247255}, doi = {http://doi.ieeecomputersociety.org/10.1109/12.485378}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Formal Verification Using EdgeValued Binary Decision Diagrams IS  2 SN  00189340 SP247 EP255 EPD  247255 A1  YungTe Lai, A1  Massoud Pedram, A1  Sarma B.K. Vrudhula, PY  1996 KW  Binary decision diagrams KW  Boolean functions KW  pseudoBoolean functions KW  verification KW  VL  45 JA  IEEE Transactions on Computers ER   
AbstractIn this paper we present a new data structure called EdgeValued BinaryDecision Diagrams (
[1] G.V. Bochmann, "Hardware specification with temporal logic: An example," IEEE Trans. Computers, vol. 31, no. 3, pp. 223231, Mar. 1982.
[2] R.T. Boute, "Representational and denotational semantics of digital systems," IEEE Trans. Computers, vol. 38, no. 7, pp. 986999, July 1989.
[3] K.S. Brace, R.L. Rudell, and R.E. Bryant, Efficient Implementation of a BDD Package Proc. Design Automation Conf., pp. 4045, 1990.
[4] R.E. Bryant, "GraphBased Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C35, No. 8, Aug. 1986, pp. 667690.
[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. 916. ACM/IEEE, June 1987.
[6] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered BinaryDecision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293318, 1992.
[7] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finitestate concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244263, 1986.
[8] E.M. Clarke, M. Fujita, P.C. McGeer, K.L. McMillan, and J.C.Y. Yang, "Multiterminal binary decision diagrams: An efficient data structure for matrix representation," Int'l Workshop Logic Synthesis, pp. 6a:115, 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. 5460, 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 higherorder logic is a good formalism for specifying and verifying hardware," Formal Aspects of VLSI Designs, G.J. Milne and P.A. Subrahmanyam, eds., pp. 153177, 1986.
[12] P.L. Hammer and S. Rudeanu, Boolean Methods in Operations Research and Related Areas.Heidelberg: SpringerVerlag, 1968.
[13] YT. Lai and S. Sastry (S.B.K. Vrudhula), "Edgevalued binary decision diagrams for multilevel hierarchical verification," Proc. 29th Design Automation Conf., pp. 608613, 1992.
[14] R.J. Bayardo, “Efficiently Mining Long Patterns From Databases,” ACM SIGMOD Conf. Management of Data, June 1998.
[15] YT. 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. 642647, 1993.
[16] YT. 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] YT. 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, “EVBDDBased Algorithms for Integer Linear Programming, Spectral Transformation, and Functional Decomposition,” IEEE Trans. ComputerAided Design of Integrated Circuits and Systems, vol. 13, no. 8, pp. 959975, Aug. 1994.
[19] HT. Liaw and CS Lin, "On the OBDDrepresentation of general Boolean functions," IEEE Trans. Computers, vol. 41, no. 6, pp. 661664, 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. 270298, 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. 9295, 1990.
[22] Texas Instruments, "The TTL data book for design engineers," Texas Instruments, 1984.