Algorithms for solving Boolean satisfiability in combinational circuits

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Algorithms for solving Boolean satisfiability in combinational circuits

Full text

Pdf (37 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. 107

Year of Publication: 1999

ISBN:1-58113-121-6

Authors

Luís Guerra e Silva	Cadence European Labs/INESC, Instituto Superior Técnico, Liboa, Portugal
L. Miguel Silveira	Cadence European Labs/INESC, Instituto Superior Técnico, Liboa, Portugal
Joöa Marques-Silva	Cadence European Labs/INESC, Instituto Superior Técnico, Liboa, Portugal

Sponsor

SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 10, Citation Count: 8

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.307557 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] M. Abramovici, M. A. Breuer and A. D. Friedman, Digital Systems Testing and Testable Design, Computer Science Press, 1990.
	2	[2] P. Barth, "A Davis-Putnam Enumeration Algorithm for Linear pseudo-Boolean Optimization," Technical Report MPI-I-95-2-003, Max Planck Institute for Computer Science, 1995.
	3	[3] 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.
	4	[4] F. Brglez and H. Fujiwara, "A Neutral List of 10 Combinational Benchmark Circuits and a Target Translator in FORTRAN," in Proc. of the Int'l Symp. on Circuits and Systems, 1985.
	5	Chih-Ang Chen , Sandeep K. Gupta, A satisfiability-based test generator for path delay faults in combinational circuits, Proceedings of the 33rd annual conference on Design automation, p.209-214, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240557]
	6	Olivier Coudert, On solving covering problems, Proceedings of the 33rd annual conference on Design automation, p.197-202, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240555]
	7	[7] S. Devadas, K. Keutzer and S. Malik, "Computation of Floating Mode Delay in Combinational Circuits: Practice and Implementation," IEEE Trans. on Computer Aided Design of Integrated Circuits and Systems, vol. 12 no. 12, pp. 1923-1936, December 1993.
	8	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]
	9	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 [doi>10.1145/288548.288619]
	10	An Exact Solution to the Minimum Size Test Pattern Problem, Proceedings of the International Conference on Computer Design, p.510, October 05-05, 1998
	11	[11] R. Fuhrer and S. Nowick, "Exact Optimal State Minimization for 2- Level Output Logic," in Int'l Workshop on Logic Synthesis, June 1998.
	12	[12] L. Guerra e Silva, J. Marques-Silva, L. M. Silveira and K. A. Sakallah, "Satisfiability Models and Algorithms for Circuit Delay Computation," in Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU), December 1997.
	13	Gary D. Hachtel , Fabio Somenzi, Logic Synthesis and Verification Algorithms, Kluwer Academic Publishers, Norwell, MA, 2000
	14	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
	15	[15] T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability," IEEE Trans. on Computer-Aided Design, vol. 11, no. 1, pp. 4-15, January 1992.
	16	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
	17	Joao P. Marques Silva , Karem A. Sakallah, Robust Search Algorithms for Test Pattern Generation, Proceedings of the 27th International Symposium on Fault-Tolerant Computing (FTCS '97), p.152, June 25-27, 1997
	18	[18] P. McGeer, A. Saldanha, P. R. Stephan, R. K. Brayton and A. L. Sangiovanni-Vincentelli, "Timing Analysis and Delay-Test Generation Using Path Recursive Functions," in Proc. of the Int'l Conf. on Computer-Aided Design, pp. 180-183, November 1991.
	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, September 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 8

	Priyank Kalla , Zhihong Zeng , Maciej J. Ciesielski , Chilai Huang, A BDD-based satisfiability infrastructure using the unate recursive paradigm, Proceedings of the conference on Design, automation and test in Europe, p.232-236, March 27-30, 2000, Paris, France
	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
	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
	Paul Tafertshofer , Andreas Ganz, SAT based ATPG using fast justification and propagation in the implication graph, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.139-146, November 07-11, 1999, San Jose, California, United States
	David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005
	Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001
	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
	Francisco Azevedo, Cardinal: A Finite Sets Constraint Solver, Constraints, v.12 n.1, p.93-129, March 2007