Using SAT for combinational equivalence checking

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Using SAT for combinational equivalence checking

Full text

Pdf (116 KB)

Source

Design, Automation, and Test in Europe archive
Proceedings of the conference on Design, automation and test in Europe table of contents

Munich, Germany

Pages: 114 - 121

Year of Publication: 2001

ISBN:0-7695-0993-2

Authors

E. Goldberg	Cadence Berkeley Laboratories, Cadence Design Systems
M. Prasad	Department of Electrical Engineering & Computer Sciences, University of California, Berkeley
R. Brayton	Department of Electrical Engineering & Computer Sciences, University of California, Berkeley

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
ECSI :
IEEE-CS\DATC : IEEE Computer Society
RAS : RAS
EDAC : Electronic Design Automation Consortium
IEEE-CS\TTTC : Test Technology Technical Council
IFIP WG 10.5 : IFIP WG 10.5
EDAA : European Design Automation Association

Publisher

IEEE Press Piscataway, NJ, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 26, Citation Count: 16

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

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 IEEE/ACM International Conference on Computer-Aided Design, pages 456- 459, November 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	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 [doi>10.1145/288548.289088]
	5	Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
	6	M. K. Ganai and A. Kuehlmann. On-the-fly compression of logical circuits. In IEEE/ACM International Workshop on Logic Synthesis, May 2000.
	7	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]
	8	Jawahar Jain , Amit Narayan , M. Fujital , A. Sangiovanni-Vincentelli, Formal Verification of Combinational Circuit, Proceedings of the Tenth International Conference on VLSI Design: VLSI in Multimedia Applications, p.218, January 04-07, 1997
	9	Joonyoung Kim , Jesse Whittemore , João P. Marques-Silva , Karem Sakallah, On applying incremental satisfiability to delay fault testing, Proceedings of the conference on Design, automation and test in Europe, p.380-384, March 27-30, 2000, Paris, France [doi>10.1145/343647.343801]
	10	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]
	11	Wolfgang Kunz, HANNIBAL: an efficient tool for logic verification based on recursive learning, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.538-543, November 07-11, 1993, Santa Clara, California, United States
	12	Wolfgang Kunz , Dominik Stoffel , Vishwani D. Agrawal , Randal E. Bryant, Reasoning in Boolean Networks: Logic Synthesis and Verification Using Testing Techniques, Kluwer Academic Publishers, Norwell, MA, 1997
	13	J. Marques-Silva and L. G. e Silva. Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning. In Workshop notes of The International Workshop on Logic Synthesis, pages 227-241, June 1999.
	14	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 [doi>10.1145/307418.307477]
	15	João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
	16	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]
	17	Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation, Proceedings of the 2000 IEEE International Conference on Computer Design: VLSI in Computers & Processors, p.459, September 17-20, 2000
	18	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
	19	G. Stalm~rck. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula, 1989. Swedish Patent 467 076 (1992), US Patent 5 276 897 (1994), European Patent 0 403 454 (1995).
	20	Paul Tafertshofer , Andreas Ganz , Manfred Henftling, A SAT-based implication engine for efficient ATPG, equivalence checking, and optimization of netlists, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.648-655, November 09-13, 1997, San Jose, California, United States
	21	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 16

	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
	Alexander Smith , Andreas Veneris , Anastasios Viglas, Design diagnosis using Boolean satisfiability, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.218-223, January 27-30, 2004, Yokohama, Japan
	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
	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
	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
	Bryan Catanzaro , Kurt Keutzer , Bor-Yiing Su, Parallelizing CAD: a timely research agenda for EDA, Proceedings of the 45th annual conference on Design automation, June 08-13, 2008, Anaheim, California
	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
	Eugene Goldberg , Yakov Novikov, BerkMin: A fast and robust Sat-solver, Discrete Applied Mathematics, v.155 n.12, p.1549-1561, June, 2007
	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
	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
	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
	Yakov Novikov, Local Search for Boolean Relations on the Basis of Unit Propagation, Proceedings of the conference on Design, Automation and Test in Europe, p.10810, March 03-07, 2003
	Alan Mishchenko , Robert K. Brayton, SAT-Based Complete Don't-Care Computation for Network Optimization, Proceedings of the conference on Design, Automation and Test in Europe, p.412-417, March 07-11, 2005
	Yexin Zheng , Michael S. Hsiao , Chao Huang, SAT-based equivalence checking of threshold logic designs for nanotechnologies, Proceedings of the 18th ACM Great Lakes symposium on VLSI, May 04-06, 2008, Orlando, Florida, USA
	Shih-Chieh Wu , Chun-Yao Wang , Yung-Chih Chen, Novel probabilistic combinational equivalence checking, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.16 n.4, p.365-375, April 2008
	Neil Kettle , Andy King, Bit-precise reasoning with affine functions, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, July 07-14, 2008, Princeton, New Jersey