A BDD-based satisfiability infrastructure using the unate recursive paradigm

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A BDD-based satisfiability infrastructure using the unate recursive paradigm

Full text

Publisher Site , Pdf

Pdf (97 KB)

Source

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

Paris, France

Pages: 232 - 236

Year of Publication: 2000

ISBN:1-58113-244-1

Authors

Priyank Kalla	Department of Electrical and Computer Engineering, University of Massachusetts at Amherst, Amherst, MA
Zhihong Zeng	Department of Electrical and Computer Engineering, University of Massachusetts at Amherst, Amherst, MA
Maciej J. Ciesielski	Department of Electrical and Computer Engineering, University of Massachusetts at Amherst, Amherst, MA
Chilai Huang	Avery Design Systems, Inc., 2 Atwood Lane, Andover, MA

Sponsors

EDAA : European Design Automation Association
SIGDA: ACM Special Interest Group on Design Automation
ECSI :
RAS : RAS
EDAC : Electronic Design Automation Consortium
IEEE-CS : Computer Society
IFIP : International Federation for Information Processing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 11, Citation Count: 4

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/343647.343769 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	Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
	2	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]
	3	C E Blair , R G Jeroslow , J K Lowe, Some results and experiments in programming techniques for propositional logic, Computers and Operations Research, v.13 n.5, p.633-645, May 1986 [doi>10.1016/0305-0548(86)90056-0]
	4	Jon William Freeman, Improvements to propositional satisfiability search algorithms, University of Pennsylvania, Philadelphia, PA, 1995
	5	Tracy Larrabee, Efficient generation of test patterns using Boolean satisfiability, Stanford University, Stanford, CA, 1990
	6	P.R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Combinational Test Generation using Satisfiability", Technical Report UCB/ERL M92/112, Dept. of EECS., Univ. of California at Berkeley, Oct. 1992.
	7	R. Zabih and D. A. McAllester, "A Rearrangement Search Strategy for Determining Propositional Satisfiability", in P~vc. Natl. Conf. on AI, 1988.
	8	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
	9	Luís Guerra e Silva , L. Miguel Silveira , Joöa Marques-Silva, Algorithms for solving Boolean satisfiability in combinational circuits, Proceedings of the conference on Design, automation and test in Europe, p.107-es, January 1999, Munich, Germany [doi>10.1145/307418.307557]
	10	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]
	11	Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
	12	Pranav Ashar , Abhijit Ghosh , Srinivas Devadas, Boolean Satisfiability and Equivalence Checking Using General Binary Decision Diagrams, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.259-264, October 14-16, 1991
	13	S. Jeong and F. Somenzi, "A New Algorithm for the Binate Covering Problem and its Application to the Minimization of Boolean Relations", in ICCAD, 92.
	14	B. Lin and F. Somenzi, "Minimization of Symbolic Relations", in ICCAD, 90.
	15	T. Villa and et al., "Explicit and Implicit Algorithms for Binate Covering Problems", IEEE Trans. CAD, vol. Vol. 16, pp. 677-691, July 1997.
	16	Alan J. Hu , Gary York , David L. Dill, New techniques for efficient verification with implicitly conjoined BDDs, Proceedings of the 31st annual conference on Design automation, p.276-282, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196377]
	17	Alan J. Hu , David L. Dill, Reducing BDD size by exploiting functional dependencies, Proceedings of the 30th international conference on Design automation, p.266-271, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164888]
	18	Amit Narayan , Jawahar Jain , M. Fujita , A. Sangiovanni-Vincentelli, Partitioned ROBDDs—a compact, canonical and efficiently manipulable representation for Boolean functions, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.547-554, November 10-14, 1996, San Jose, California, United States
	19	Robert King Brayton , Alberto L. Sangiovanni-Vincentelli , Curtis T. McMullen , Gary D. Hachtel, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Norwell, MA, 1984
	20	R. Rudell and A. Sangiovanni-Vincentelli, "Multiple-valued Minimization for PLA Optimization", IEEE T~: on CAD, vol. CAD-6, pp. 727-750, Sept. 1987.
	21	C.L. Huang, "Private Communication", Avery Design Systems, Inc.
	22	F. Brown, Boolean Reasoning, Kluwer Academic Publishers, 1990.
	23	Gary D. Hachtel , Fabio Somenzi, Logic Synthesis and Verification Algorithms, Kluwer Academic Publishers, Norwell, MA, 2000
	24	G. DeMicheli, Synthesis and Optimization of Digital Circuits, McGraw-Hill, 94.
	25	Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Stefano Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, Proceedings of the 34th annual conference on Design automation, p.728-733, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266355]
	26	Farzan Fallah , Srinivas Devadas , Kurt Keutzer, Functional vector generation for HDL models using linear programming and 3-satisfiability, Proceedings of the 35th annual conference on Design automation, p.528-533, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277187]

CITED BY 4

	Z. Zeng , P. Kalla , M. Ciesielski, LPSAT: a unified approach to RTL satisfiability, Proceedings of the conference on Design, automation and test in Europe, p.398-402, March 2001, Munich, Germany
	Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, Journal of Symbolic Computation, v.35 n.2, p.73-106, February 2003
	Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW, Proceedings of the 38th conference on Design automation, p.226-231, June 2001, Las Vegas, Nevada, United States
	Zhihong Zeng , Kesava R. Talupuru , Maciej Ciesielski, Functional test generation based on word-level SAT, Journal of Systems Architecture: the EUROMICRO Journal, v.51 n.8, p.488-511, August 2005