Equivalence checking using cuts and heaps

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Equivalence checking using cuts and heaps

Full text

Pdf (229 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 34th annual Design Automation Conference table of contents

Anaheim, California, United States

Pages: 263 - 268

Year of Publication: 1997

ISBN:0-89791-920-3

Authors

Andreas Kuehlmann	IBM Thomas J. Watson Research Center, Yorktown Heights, NY
Florian Krohm	IBM Thomas J. Watson Research Center, Yorktown Heights, NY

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): 41, Citation Count: 47

Additional Information:

abstract 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/266021.266090 What is a DOI?

ABSTRACT

This paper presents a verification technique which isspecifically targeted to formally comparing large combinational circuits with some structural similarities. The approach combines the application of BDDs withcircuit graph hashing, automatic insertion of multiple cut frontiers, and a controlled elimination of false negative verification results caused by the cuts. Twoideas fundamentally distinguish the presented technique from previous approaches. First, originating from the cut frontiers, multiple BDDs are computedfor the internal nets of the circuit, and second, theBDD propagation is prioritized by size and discontinued once a given limit is exceeded.

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	G. L. Smith, R. J. Bahnsen, and H. Halliwell, "Boolean comparison of hardware and flowcharts," IBM Journal of Research and Development, vol. 26, pp. 106-116, January 1982.
	2	D. P. Appenzeller, Formal verification of a PowerPC microprocessor, Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and Processors, p.79, October 02-04, 1995
	3	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]
	4	C. L. Berman and L. H. Trevillyan, "Functional comparison of logic designs for VLSI circuits," in Digest of Technical Papers of the IEEE International Conference on Computer-Aided Design, pp. 456-459, IEEE, November 1989.
	5	C. A. J. van Eijk , Geert Janssen, Exploiting Structural Similarities in a BDD-Based Verification Method, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.110-125, September 26-28, 1994
	6	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]
	7	Subdodh M. Reddy , Wolfgang Kunz , Dhiraj K. Pradhan, Novel verification framework combining structural and OBDD methods in a synthesis environment, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.414-419, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.328705]
	8	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
	9	A. Kuehlmann , A. Srinivasan , D. P. LaPotin, Verity—a formal verification program for custom CMOS circuits, IBM Journal of Research and Development, v.39 n.1-2, p.149-165, Jan./March 1995
	10	Florian Krohm , Andreas Kuchlmann , Arjen Mets, The use of random simulation in formal verification, Proceedings of the 1996 International Conference on Computer Design, VLSI in Computers and Processors, p.371, October 07-09, 1996

CITED BY 47

	Andreas Kuehlmann , Cornelis A. J. van Eijk, Combinational and sequential equivalence checking, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Rajarshi Mukherjee , Jawahar Jain , Koichiro Takayama , Masahiro Fujita, Automatic partitioning for efficient combinatorial verification, Proceedings of the 2000 conference on Asia South Pacific design automation, p.67-72, January 2000, Yokohama, Japan
	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
	Reinaldo A. Bergamaschi , John Cohn, The A to Z of SoCs, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.790-798, November 10-14, 2002, San Jose, California
	R. Reetz , K. Schneider , T. Kropf, Formal specification in VHDL for hardware verification, Proceedings of the conference on Design, automation and test in Europe, p.257-265, February 23-26, 1998, Le Palais des Congrés de Paris, France
	Malay K. Ganai , Adnan Aziz , Andreas Kuehlmann, Enhancing simulation with BDDs and ATPG, Proceedings of the 36th ACM/IEEE conference on Design automation, p.385-390, June 21-25, 1999, New Orleans, Louisiana, United States
	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
	Demos Anastasakis , Robert Damiano , Hi-Keung Tony Ma , Ted Stanion, A practical and efficient method for compare-point matching, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Jerry R. Burch , Vigyan Singhal, Tight integration of combinational verification methods, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.570-576, November 08-12, 1998, San Jose, California, United States
	F. Ferrandi , A. Macii , E. Macii , M. Poncino , R. Scarsi , F. Somenzi, Symbolic algorithms for layout-oriented synthesis of pass transistor logic circuits, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.235-241, November 08-12, 1998, San Jose, California, United States
	Jerry R. Burch , Vigyan Singhal, Robust latch mapping for combinational equivalence checking, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.563-569, November 08-12, 1998, San Jose, California, United States
	Christoph Scholl , Bernd Becker, Checking equivalence for partial implementations, Proceedings of the 38th conference on Design automation, p.238-243, June 2001, Las Vegas, Nevada, United States
	Armin Biere , Wolfgang Kunz, SAT and ATPG: Boolean engines for formal hardware verification, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.782-785, November 10-14, 2002, San Jose, California
	Anuj Goel , Khurram Sajid , Hai Zhou , Adnan Aziz , Vigyan Singhal, BDD Based Procedures for a Theory of Equality with Uninterpreted Functions, Formal Methods in System Design, v.22 n.3, p.205-224, May 2003
	Dominik Stoffel , Wolfgang Kunz, Verification of integer multipliers on the arithmetic bit level, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Auxiliary variables for BDD-based representation and manipulation of Boolean functions, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.3 n.3, p.309-340, July 1998
	Harry Foster, Applied Boolean Equivalence Verification and RTL Static Sign-Off, IEEE Design & Test, v.18 n.4, p.6-15, July 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 , 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
	Feng Lu , Li-C. Wang , K.-T. (Tim) Cheng , John Moondanos , Ziyad Hanna, A signal correlation guided ATPG solver and its applications for solving difficult industrial cases, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
	Wolfgang Günther , Rolf Drechsler, Efficient Minimization and Manipulation of Linearly Transformed Binary Decision Diagrams, IEEE Transactions on Computers, v.52 n.9, p.1196-1209, September 2003
	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
	Andreas Veneris , Alexander Smith , Magdy S. Abadir, Logic verification based on diagnosis techniques, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
	Stefano Quer , Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Ellen M. Sentovich , Robert K. Brayton, Verification of Similar FSMs by Mixing Incremental Re-encoding, Reachability Analysis, and Combinational Checks, Formal Methods in System Design, v.17 n.2, p.107-134, Oct. 2000
	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
	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
	Xiushan Feng , Alan J. Hu, Cutpoints for formal equivalence verification of embedded software, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA
	Masahiro Fujita, Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.10 n.4, p.610-626, October 2005
	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
	Hee Hwan Kwak , In-Ho Moon , James H. Kukula , Thomas R. Shiple, Combinational equivalence checking through function transformation, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.526-533, November 10-14, 2002, San Jose, California
	Wei Huang , PuShan Tang , Min Ding, Sequential equivalence checking using cuts, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
	Xiushan Feng , Alan J. Hu, Early cutpoint insertion for high-level software vs. RTL formal combinational equivalence verification, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
	Tejaswi Gowda , Sarma Vrudhula , Goran Konjevod, Combinational equivalence checking for threshold logic circuits, Proceedings of the 17th great lakes symposium on Great lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy
	Qi Zhu , Nathan Kitchen , Andreas Kuehlmann , Alberto Sangiovanni-Vincentelli, SAT sweeping with local observability don't-cares, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
	Michael L. Case , Victor N. Kravets , Alan Mishchenko , Robert K. Brayton, Merging nodes under sequential observability, Proceedings of the 45th annual conference on Design automation, June 08-13, 2008, Anaheim, California
	P. Bjesse , A. Boralv, DAG-aware circuit compression for formal verification, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.42-49, November 07-11, 2004
	A. Kuehlmann, Dynamic transition relation simplification for bounded property checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.50-57, November 07-11, 2004
	Jaehong Park , Carl Pixley , Michael Burns , Hyunwoo Cho, An Efficient Logic Equivalence Checker for Industrial Circuits, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.91-106, Feb/April 2000
	Rajarshi Mukherjee , Jawahar Jain , Koichiro Takayama , Masahiro Fujita , Jacob A. Abraham , Donald S. Fussell, An efficient filter-based approach for combinational verification, Proceedings of the conference on Design, automation and test in Europe, p.31-es, January 1999, Munich, Germany
	João Marques-Silva , Thomas Glass, Combinational equivalence checking using satisfiability and recursive learning, Proceedings of the conference on Design, automation and test in Europe, p.33-es, January 1999, Munich, Germany
	Hans Eveking , Holger Hinrichsen , Gerd Ritter, Automatic verification of scheduling results in high-level synthesis, Proceedings of the conference on Design, automation and test in Europe, p.12-es, January 1999, Munich, Germany
	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
	Satrajit Chatterjee , Alan Mishchenko , Robert Brayton , Andreas Kuehlmann, On resolution proofs for combinational equivalence, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California
	Malay K. Ganai , Adnan Aziz, Improved SAT-based Bounded Reachability Analysis, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.729, January 07-11, 2002
	Gianpiero Cabodi , Marco Crivellari , Sergio Nocco , Stefano Quer, Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking, Proceedings of the conference on Design, Automation and Test in Europe, p.688-689, March 07-11, 2005
	Jason Baumgartner , Andreas Kuehlmann, Enhanced Diameter Bounding via Structural, Proceedings of the conference on Design, automation and test in Europe, p.10036, February 16-20, 2004
	Eric Whitman Smith , David L. Dill, Automatic formal verification of block cipher implementations, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-7, November 17-20, 2008, Portland, Oregon