Circuit-based Boolean Reasoning

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Circuit-based Boolean Reasoning

Full text

Pdf (146 KB)

Source

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

Las Vegas, Nevada, United States

Pages: 232 - 237

Year of Publication: 2001

ISBN:1-58113-297-2

Authors

Andreas Kuehlmann	Cadence Berkeley Labs, Berkeley, CA
Malay K. Ganai	The University of Texas at Austin, Austin, TX
Viresh Paruthi	IBM Enterprise Systems Group, Austin, TX

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): 5, Downloads (12 Months): 31, Citation Count: 29

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

ABSTRACT

Many tasks in CAD, such as equivalence checking, property checking, logic synthesis, and false paths analysis require efficient Boolean reasoning for problems derived from circuit structures. Traditionally, canonical representations, e. g., BDDs, or SAT- based search methods are used to solve a particular class of problems. In this paper we present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, and a SAT procedure natively working on a shared graph representation of the problem. The described intertwined integration of the three techniques results in a robust summation of their orthogonal strengths. Our experiments demonstrate the effectiveness of the approach.

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	M. K. Ganai and A. Kuehlmann, "On-the-fly compression of logical circuits," Tech. Rep. Computer Science, RC 21704, IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY 10598, March 2000.
	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	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]
	4	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
	5	Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
	6	João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
	7	S. B. Akers, "Binary decision diagrams," IEEE Transactions on Computers, vol. 27, pp. 509-516, June 1978.
	8	S.-W. Jeong, B. Plessier, G. Hachtel, and F. Somenzi, "Extended BDD's: Trading off canonicity for structure in verification algorithms," in Digest of Technical Papers of the IEEE International Conference on Computer-Aided Design, pp. 464-467, IEEE, November 1991.
	9	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.
	10	H. Hulgaard, P. Williams, and H. Andersen, "Equivalence checking of combinational circuits using Boolean expression diagrams," IEEE Transactions on Computer-Aided Design, vol. 18, July 1999.
	11	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]
	12	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
	13	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]
	14	Sandip Kundu , Leendert M. Huisman , Indira Nair , Vijay S. Iyengar , Lakshmi N. Reddy, A Small Test Generator for Large Designs, Proceedings of the IEEE International Test Conference on Discover the New World of Test and Design, p.30-40, September 20-24, 1992

CITED BY 29

	Andreas Kuehlmann , Cornelis A. J. van Eijk, Combinational and sequential equivalence checking, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Slawomir Pilarski , Gracia Hu, SAT with partial clauses and back-leaps, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Malay K. Ganai , Pranav Ashar , Aarti Gupta , Lintao Zhang , Sharad Malik, Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	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
	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
	Miroslav N. Velev, Efficient translation of boolean formulas to CNF in formal verification of microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.310-315, January 27-30, 2004, Yokohama, Japan
	Jason Baumgartner , Andreas Kuehlmann, Min-area retiming on flexible circuit structures, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	Robert K. Brayton, The future of logic synthesis and verification, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Matti Järvisalo , Tommi Junttila , Ilkka Niemelä, Unrestricted vs restricted cut in a tableau method for Boolean circuits, Annals of Mathematics and Artificial Intelligence, v.44 n.4, p.373-399, August 2005
	Chi-An Wu , Ting-Hao Lin , Chih-Chun Lee , Chung-Yang (Ric) Huang, QuteSAT: a robust circuit-based SAT solver for complex circuit structure, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
	M. K. Ganai , A. Gupta , P. Ashar, Efficient SAT-based unbounded symbolic model checking using circuit cofactoring, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.510-517, November 07-11, 2004
	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
	F. Zaraket , J. Baumgartner , A. Aziz, Scalable compositional minimization via static analysis, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1060-1067, November 06-10, 2005, San Jose, CA
	R. Drechsler, Using Word-Level Information in Formal Hardware Verification, Automation and Remote Control, v.65 n.6, p.963-977, June 2004
	E. Dubrova , M. Teslenko , A. Martinelli, Kauffman networks: analysis and applications, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.479-484, November 06-10, 2005, San Jose, CA
	G. Parthasarathy , M. K. Iyer , K.-T. Cheng , F. Brewer, RTL SAT simplification by Boolean and interval arithmetic reasoning, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.297-302, November 06-10, 2005, San Jose, CA
	Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar, Iterative Abstraction using SAT-based BMC with Proof Analysis, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.416, November 09-13, 2003
	Feng Lu , Li-C. Wang , Kwang-Ting Cheng , Ric C-Y Huang, A Circuit SAT Solver With Signal Correlation Guided Learning, Proceedings of the conference on Design, Automation and Test in Europe, p.10892, March 03-07, 2003
	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
	Zhaohui Fu , Yinlei Yu , Sharad Malik, Considering Circuit Observability Don't Cares in CNF Satisfiability, Proceedings of the conference on Design, Automation and Test in Europe, p.1108-1113, 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
	Miroslav N. Velev, Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors, Proceedings of the conference on Design, automation and test in Europe, p.10266, February 16-20, 2004
	Sean Safarpour , Andreas Veneris , Rolf Drechsler , Joanne Lee, Managing Don't Cares in Boolean Satisfiability, Proceedings of the conference on Design, automation and test in Europe, p.10260, February 16-20, 2004
	Jochen Eisinger , Felix Klaedtke, Don't care words with an application to the automata-based approach for real addition, Formal Methods in System Design, v.33 n.1-3, p.85-115, December 2008
	Matti Järvisalo , Tommi Junttila , Ilkka Niemelä, Justification-Based Non-Clausal Local Search for SAT, Proceeding of the 2008 conference on ECAI 2008: 18th European Conference on Artificial Intelligence, p.535-539, June 27, 2008
	Matti Järvisalo , Tommi Junttila, Limitations of restricted branching in clause learning, Constraints, v.14 n.3, p.325-356, September 2009
	Matti Järvisalo , Tommi Junttila, On the power of top-down branching heuristics, Proceedings of the 23rd national conference on Artificial intelligence, p.304-309, July 13-17, 2008, Chicago, Illinois