Reducing BDD size by exploiting functional dependencies

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Reducing BDD size by exploiting functional dependencies

Full text

Pdf (733 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 30th international Design Automation Conference table of contents

Dallas, Texas, United States

Pages: 266 - 271

Year of Publication: 1993

ISBN:0-89791-577-1

Authors

Alan J. Hu
David L. Dill

Sponsors

EDAC : Electronic Design Automation Consortium
IEEE-CAS : Circuits & Systems
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 22, Citation Count: 16

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/157485.164888 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	S. Bose and A. Fisher, "Automatic Verification of Synchronous Circuits Using Symbolic Logic Simulation and Temporal Logic," IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, Luc J.M. Claesen, ed., North Holland, 1989.
	2	Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
	3	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	4	Randal E. Bryant, On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication, IEEE Transactions on Computers, v.40 n.2, p.205-213, February 1991 [doi>10.1109/12.73590]
	5	J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
	6	J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, "Symbolic Model Checking: 1020 States and Beyond," Proceedings of the Conference on Logic in Computer Science, 1990, pp. 428-439.
	7	K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
	8	Massimiliano Chiodo , Thomas R. Shiple , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Automatic compositional minimization in CTL model checking, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.172-178, November 1992, Santa Clara, California, United States
	9	O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
	10	Olivier Coudert, Christian Berthet, and Jean Christophe Madre,"Verification of Sequential Machines Using Boolean Functional Vectors," IMEC- IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, Luc J.M. Claesen, ed., North Holland, 1989.
	11	David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
	12	Alan J. Hu , David L. Dill , Andreas Drexler , C. Han Yang, Higher-Level Specification and Verification with BDDs, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.82-95, June 29-July 01, 1992
	13	S.-W. Jeong, B. Plessier, G.D. Hachtel, and E Somenzi, "Variable Ordering for FSM Traversal," Proceedings of the International Workshop on Logic Synthesis, MCNC, Research Triangle Park, NC, May 1991.
	14	Timothy Y. K. Kam and Robert K. Brayton, "Multi-Valued Decision Diagrams," UCB/ERL M90/125, December 1990.
	15	Y.-T. Lai , S. Sastry, Edge-valued binary decision diagrams for multi-level hierarchical verification, Proceedings of the 29th ACM/IEEE conference on Design automation, p.608-613, June 08-12, 1992, Anaheim, California, United States
	16	K. L. McMillan and J. Schwalbe, "Formal Verification of the Gigamax Cache-Consistency Protocol," Proceedings of the International Symposium on Shared Memory Multiprocessing, Information Processing Society of Japan, 1991, pp. 242-251.
	17	Arvind Srinivasan, Timothy Kam, Sharad Malik, and Robert K. Brayton, "Algorithms for Discrete Function Manipulation," IEEE International Conference on Computer-Aided Design, 1990, pp. 92-95.
	18	Herve J. Touati, Hamid Savoj, Bill Lin, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli, "Implicit State Enumeration of Finite State Machines using BDD's" IEEE International Conference on Computer-Aided Design, 1990, pp. 130-133.

CITED BY 16

	Jörg Bormann , Jörg Lohse , Michael Payer , Gerd Venzl, Model checking in industrial hardware design, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.298-303, June 12-16, 1995, San Francisco, California, United States
	Andreas Kuehlmann , Cornelis A. J. van Eijk, Combinational and sequential equivalence checking, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Priyank Kalla , Zhihong Zeng , Maciej J. Ciesielski , Chilai Huang, A BDD-based satisfiability infrastructure using the unate recursive paradigm, Proceedings of the conference on Design, automation and test in Europe, p.232-236, March 27-30, 2000, Paris, France
	F. Corella , Z. Zhou , X. Song , M. Langevin , E. Cerny, Multiway Decision Graphs for Automated Hardware Verification, Formal Methods in System Design, v.10 n.1, p.7-46, February 1997
	Alan J. Hu , Gary York , David L. Dill, New techniques for efficient verification with implicitly conjoined BDDs, Proceedings of the 31st annual conference on Design automation, p.276-282, June 06-10, 1994, San Diego, California, United States
	William Chan , Richard J. Anderson , Paul Beame , David Notkin, Improving efficiency of symbolic model checking for state-based system requirements, ACM SIGSOFT Software Engineering Notes, v.23 n.2, p.102-112, March 1998
	Valeria Bertacco , Maurizio Damiani , Stefano Quer, Cycle-based symbolic simulation of gate-level synchronous circuits, Proceedings of the 36th ACM/IEEE conference on Design automation, p.391-396, June 21-25, 1999, New Orleans, Louisiana, United States
	Jason Cong , Yuzheng Ding, Combinational logic synthesis for LUT based field programmable gate arrays, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.1 n.2, p.145-204, April 1996
	Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	Amit Goel , Randal E. Bryant, Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis, Proceedings of the conference on Design, Automation and Test in Europe, p.10816, March 03-07, 2003
	C. A. J. Van Eijk , J. A. G. Jess, Exploiting Functional Dependencies in Finite State Machine Verification, Proceedings of the 1996 European conference on Design and Test, p.9, March 11-14, 1996
	Chih-Chun Lee , Jie-Hong R. Jiang , Chung-Yang (Ric) Huang , Alan Mishchenko, Scalable exploration of functional dependency by interpolation and incremental SAT solving, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
	Jérôme Lang , Pierre Marquis, On propositional definability, Artificial Intelligence, v.172 n.8-9, p.991-1017, May, 2008
	Roderick Bloem , Stefan Galler , Barbara Jobstmann , Nir Piterman , Amir Pnueli , Martin Weiglhofer, Specify, Compile, Run: Hardware from PSL, Electronic Notes in Theoretical Computer Science (ENTCS), v.190 n.4, p.3-16, November, 2007
	Chen-Hsuan Lin , Chun-Yao Wang, Dependent latch identification in the reachable state space, Proceedings of the 2009 Conference on Asia and South Pacific Design Automation, January 19-22, 2009, Yokohama, Japan