Combinational equivalence checking using satisfiability and recursive learning

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Combinational equivalence checking using satisfiability and recursive learning

Full text

Pdf (40 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

Article No. 33

Year of Publication: 1999

ISBN:1-58113-121-6

Authors

João Marques-Silva	Instituto Superior Técnico, Cadence European Labs/INESC, Lisboa, Portugal
Thomas Glass	Siemens AG, Corporate Technology, Munich, Germany

Sponsor

SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 24, Citation Count: 10

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/307418.307477 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	[1] R. Bayardo Jr. and R. Schrag, "Using CSP Look-Back Techniques to Solve Real-World SAT Instances," in Proc. of the Nat'l Conf. on Artificial Intelligence, pp. 203-208, July 1997.
	2	[2] C. L. Berman and L. H. Trevillyan, "Functional Comparison of Logic Designs for VLSI Circuits," in Proc. of the Int'l Conf. on Computer-Aided Design, pp. 456-459, November 1989.
	3	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
	4	Jon William Freeman, Improvements to propositional satisfiability search algorithms, University of Pennsylvania, Philadelphia, PA, 1995
	5	Shi-Yu Huang , Kwant-Ting Cheng, Formal Equivalence Checking and Design DeBugging, Kluwer Academic Publishers, Norwell, MA, 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	[7] G. Janssen, The Eindhoven BDD Package, Eindhoven University of Technology. (URL: ftp://ftp.ics.ele.tue.nl/pub/users/geert/ bdd.tar.gz.)
	8	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]
	9	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
	10	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
	11	[11] T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability," IEEE Trans. on Computer-Aided Design, vol. 11, no. 1, pp. 4-15, January 1992.
	12	[12] S. Malik, A. R. Wang, R. K. Brayton and A. Sangiovanni-Vincentelli, "Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment", in Proc. of the Int'l Conf. e on Computer-Aided Design, pp. 6-9, November 1988.
	13	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
	14	[14] J. Marques-Silva, "Improving Satisfiability Algorithms by Using Recursive Learning," in International Workshop on Boolean Problems , September 1998.
	15	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]
	16	Shipra Panda , Fabio Somenzi , Bernard F. Plessier, Symmetry detection and dynamic variable ordering of decision diagrams, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.628-631, November 06-10, 1994, San Jose, California, United States
	17	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]
	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	[19] P. Stephan, R.K. Brayton and A.L. Sangiovanni-Vincentelli, "Combinatorial Test Generation Using Satisfiability", IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, vol. 15, no. 9, Sep. 1996.
	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	Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997

CITED BY 10

	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
	Wolfgang Kunz , João Marques-Silva , Sharad Malik, SAT and ATPG: algorithms for Boolean decision problems, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	João P. Marques-Silva , Karem A. Sakallah, Boolean satisfiability in electronic design automation, Proceedings of the 37th conference on Design automation, p.675-680, June 05-09, 2000, Los Angeles, 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
	João Marques-Silva , Luís Guerra e Silva, Solving Satisfiability in Combinational Circuits, IEEE Design & Test, v.20 n.04, p.16-21, January 2003
	Chu-Min Li, Equivalent literal propagation in the DLL procedure, Discrete Applied Mathematics, v.130 n.2, p.251-276, 15 August 2003
	Prabhat Mishra , Nikil Dutt , Narayanan Krishnamurthy , Magdy S. Abadir, A Top-Down Methodology for Microprocessor Validation, IEEE Design & Test, v.21 n.2, p.122-131, March 2004
	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
	Lucas Bordeaux , Youssef Hamadi , Lintao Zhang, Propositional Satisfiability and Constraint Programming: A comparative survey, ACM Computing Surveys (CSUR), v.38 n.4, p.12-es, 2006