New techniques for efficient verification with implicitly conjoined BDDs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

New techniques for efficient verification with implicitly conjoined BDDs

Full text

Pdf (132 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 31st annual Design Automation Conference table of contents

San Diego, California, United States

Pages: 276 - 282

Year of Publication: 1994

ISBN:0-89791-653-0

Authors

Alan J. Hu	Department of Computer Science, Stanford University
Gary York	Cadence Labs, Cadence Design Systems, Inc.
David L. Dill	Department of Computer Science, Stanford University

Sponsors

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

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 11, Citation Count: 3

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/196244.196377 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	J.R. Burch, E.M. Clarke, and D.E. Long, "Symbolic Model Checking with Partitioned Transition Relations," VLSI '91: Proceedings of the IFIP TC IO/WG 10.5 International Conference on Very Large Scale Integration, Edinburgh, Great Britain, 1991.
	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: 102o States and Beyond," Proceedings of the Conference on Logic in Computer Science, 1990, pp. 428-439.
	7	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
	8	Hyunwoo Cho, Gary Hachtel, Seh-Woong Jeong, Bernard Plessier, Eric Schwarz, and Fabio Somenzi,"ATPG Aspects of FSM Verification,"IEEE International Conference on Computer-Aided Design, 1990, pp. 134- 137.
	9	Edmund M. Clarke , Orna Grumberg , Hiromi Hiraishi , Somesh Jha , David E. Long , Kenneth L. McMillan , Linda A. Ness, Verification of the Futurebus+ Cache Coherence Protocol, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.15-30, April 26-28, 1993
	10	Olivier Coudert and Jean Christophe Madre, "A Unified Framework for the Formal Verification of Sequential Circuits," IEEE International Conference on Computer-Aided Design, 1990, pp. 126-129.
	11	Olivier Coudert , Christian Berthet , Jean Christophe 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, June 12-14, 1989
	12	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.
	13	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
	14	Thomas Filkorn, Functional Extension of Symbolic Model Checking, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.225-232, July 01-04, 1991
	15	Michael R. Garey and David S. Johnson, Computers and Intractability, W.H. Freeman and Company, 1979, p. 222.
	16	Alan J. Hu , David L. Dill, Reducing BDD size by exploiting functional dependencies, Proceedings of the 30th international conference on Design automation, p.266-271, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164888]
	17	Alan J. Hu , David L. Dill, Efficient Verification with BDDs using Implicitly Conjoined Invariants, Proceedings of the 5th International Conference on Computer Aided Verification, p.3-14, June 28-July 01, 1993
	18	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
	19	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.
	20	David E. Long, personal correspondence.
	21	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.
	22	Christos H. Papadimitriou and Kenneth Steiglitz, Combinatorial Optimization, Prentice-Hall, 1982, p. 262.
	23	Carl Pixley, Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.54-64, June 18-21, 1990
	24	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 3

	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
	Jason Baumgartner , Tamir Heyman , Vigyan Singhal , Adnan Aziz, An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists, Formal Methods in System Design, v.23 n.1, p.39-65, July 2003
	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