Tight integration of combinational verification methods

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Tight integration of combinational verification methods

Full text

Pdf (969 KB)

Source

International Conference on Computer Aided Design archive
Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design table of contents

San Jose, California, United States

Pages: 570 - 576

Year of Publication: 1998

ISBN:1-58113-008-2

Authors

Jerry R. Burch	Cadence Berkeley Labs, 2001 Addison St, 3rd Floor, Berkeley, CA
Vigyan Singhal	Cadence Berkeley Labs, 2001 Addison St, 3rd Floor, Berkeley, CA

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS : Computer Society
IEEE-EDS : Electronic Devices Society
IEEE-CAS : Circuits & Systems

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 10, Citation Count: 20

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	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/288548.289088 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	C. L. Berman and L. H. Trevillyan. Functional Comparison of Logic Designs for VLSI Circuits. In Proc. Intl. Conf. on Computer-Aided Design, pages 456-459, 1989.
	2	Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
	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. Gu, P. W. Purdom, j. V. Franco, and B. W. Wah. Algorithms for the Satisfiability (SAT) Problem: A Survey. In D. Du, J. Gu, and P. M. Pardalos, editors, Satisfiability Problems: Theory and Applications. American Mathematical Society, 1997.
	5	Aarti Gupta , Pranav Ashar, Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking, Proceedings of the Eleventh International Conference on VLSI Design: VLSI for Signal Processing, p.222, January 04-07, 1998
	6	Jawahar Jain , Rajarshi Mukherjee , Masahiro Fujita, Advanced verification techniques based on learning, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.420-426, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217564]
	7	Andreas Kuehlmann , Florian Krohm, Equivalence checking using cuts and heaps, Proceedings of the 34th annual conference on Design automation, p.263-268, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266090]
	8	W. Kunz, D. K. Pradhan, and S. Reddy. A Novel Framework for Logic Verification in a Synthesis Environment. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 15(I):20-36, January 1996.
	9	David E. Long. BDD Manipulation Library. Public software. Carnegie Mellon University, Pittsburgh, PA, June 1993. ftp : / / emc. cs. cmu. edu/pub/bdd/bddlib, tar. Z.
	10	Yusuke Matsunaga, An efficient equivalence checker for combinational circuits, Proceedings of the 33rd annual conference on Design automation, p.629-634, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240637]
	11	R. Mu "kherjee, J. Jain, K. Takayama, M. Fujita, J. A. Abraham, and D. S. Fussell. FLOVER: Flitering Oriented Combinational Verification Approach. In Workshop Notes of International Workshop on Logic Synthesis, Tahoe City, CA, 1997.
	12	Dhiraj K. Pradhan , Debjyoti Paul , Mitrajit Chatterjee, VERILAT: verification using logic augmentation and transformations, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.88-95, November 10-14, 1996, San Jose, California, United States
	13	B. Selman, H. Leveque, and D. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proc. of AAAI, pages 440--446, 1992.
	14	Ellen Sentovich , Kanwar Jit Singh , Cho W. Moon , Hamid Savoj , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Sequential Circuit Design Using Synthesis and Optimization, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.328-333, October 11-14, 1992
	15	C.A.J. van Eijk. Formal Methods for the Verification of Digital Circuits. PhD thesis, Eindhoven University of Technology, Dept. of Electrical Engineering, Eindhoven, Netherlands, 1997.

CITED BY 20

	Y. Novikov , E. Goldberg, An efficient learning procedure for multiple implication checks, Proceedings of the conference on Design, automation and test in Europe, p.127-135, March 2001, Munich, Germany
	E. Goldberg , M. Prasad , R. Brayton, Using SAT for combinational equivalence checking, Proceedings of the conference on Design, automation and test in Europe, p.114-121, March 2001, Munich, Germany
	Andreas Kuehlmann , Malay K. Ganai , Viresh Paruthi, Circuit-based Boolean Reasoning, Proceedings of the 38th conference on Design automation, p.232-237, June 2001, Las Vegas, Nevada, United States
	Andreas Kuehlmann , Cornelis A. J. van Eijk, Combinational and sequential equivalence checking, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Kelvin Ng , Mukul R. Prasad , Rajarshi Mukherjee , Jawahar Jain, Solving the latch mapping problem in an industrial setting, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
	Aarti Gupta , Anubhav Gupta , Zijiang Yang , Pranav Ashar, Dynamic detection and removal of inactive clauses in SAT with application in image computation, Proceedings of the 38th conference on Design automation, p.536-541, June 2001, Las Vegas, Nevada, United States
	Wanlin Cao , Duncan M. H. Walker , Rajarshi Mukherjee, An efficient solution to the storage correspondence problem for large sequential circuits, Proceedings of the 2001 conference on Asia South Pacific design automation, p.181-186, January 2001, Yokohama, Japan
	Aarti Gupta , Malay Ganai , Chao Wang , Zijiang Yang , Pranav Ashar, Learning from BDDs in SAT-based bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
	Harry Foster, Applied Boolean Equivalence Verification and RTL Static Sign-Off, IEEE Design & Test, v.18 n.4, p.6-15, July 2001
	S. Reda , A. Salem, Combinational equivalence checking using Boolean satisfiability and binary decision diagrams, Proceedings of the conference on Design, automation and test in Europe, p.122-126, March 2001, Munich, Germany
	Robert Damiano , James Kukula, Checking satisfiability of a conjunction of BDDs, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
	Demosthenes Anastasakis , Lisa McIlwain , Slawomir Pilarski, Efficient equivalence checking with partitions and hierarchical cut-points, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
	Aarti Gupta , Zijiang Yang , Pranav Ashar , Lintao Zhang , Sharad Malik, Partition-based decision heuristics for image computation using SAT and BDDs, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	Katarzyna Radecka , Zeljko Zilic, Design Verification by Test Vectors and Arithmetic Transform Universal Test Set, IEEE Transactions on Computers, v.53 n.5, p.628-640, May 2004
	Ronald P. Lajaunie , Michael S. Hsiao, An effective and efficient ATPG-based combinational equivalence checker, Proceedings of the 15th ACM Great Lakes symposium on VLSI, April 17-19, 2005, Chicago, Illinois, USA
	Eugene Goldberg, On equivalence checking and logic synthesis of circuits with a common specification, Proceedings of the 15th ACM Great Lakes symposium on VLSI, April 17-19, 2005, Chicago, Illinois, USA
	Gunnar Andersson , Per Bjesse , Byron Cook , Ziyad Hanna, A proof engine approach to solving combinational design automation problems, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Eugene Goldberg , Yakov Novikov, BerkMin: A fast and robust Sat-solver, Discrete Applied Mathematics, v.155 n.12, p.1549-1561, June, 2007
	Malay Ganai , Praveen Yalagandula , Adnan Aziz , Andreas Kuehlmann , Vigyan Singhal, SIVA: A System for Coverage-Directed State Space Search, Journal of Electronic Testing: Theory and Applications, v.17 n.1, p.11-27, February 2001
	Evgueni Goldberg , Yakov Novikov, Verification of Proofs of Unsatisfiability for CNF Formulas, Proceedings of the conference on Design, Automation and Test in Europe, p.10886, March 03-07, 2003