On the relation between simulation-based and SAT-based diagnosis

ABSTRACT

The problem of diagnosis -- or locating the source of an error or fault -- occurs in several areas of computer aided design, such as dynamic verification, property checking, equivalence checking and production test. Manually locating errors can be a time consuming and resource-intensive process. Several automated approaches for diagnosis have been presented, among them are simulation-based and SAT-based techniques. These two approaches are found to be robust even for large circuits as well as being applicable to a broad range of diagnosis problems. An in-depth comparison of both approaches necessary to augment our knowledge of diagnosis procedures has not been addressed by previous work.This paper provides a thorough analysis of the similarities and differences between simulation-based and SAT-based procedures for diagnosis. The relation between the basic approaches is theoretically analyzed. Issues regarding performance and diagnosis quality (resolution) are discussed. Experimental data strengthens the theoretical results. This detailed understanding of the relations between the techniques is necessary to provide further improvements to the field of diagnosis. The initial steps towards building a hybrid technique are also presented.

REFERENCES

• 1: M. S. Abadir, J. Ferguson, and T. Kirkland. Logic verification via test generation. IEEE Trans. on CAD, 7:172--177, 1988.
• 2: M. Abramovici , P. R. Menon , D. T. Miller, Critical path tracing - an alternative to fault simulation, Proceedings of the 20th conference on Design automation, p.214-220, June 27-29, 1983, Miami Beach, Florida, United States
• 3: M. F. Ali , S. Safarpour , A. Veneris , M. S. Abadir , R. Drechsler, Post-verification debugging of hierarchical designs, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.871-876, November 06-10, 2005, San Jose, CA
• 4: M. Fahim Ali , A. Veneris , A. Smith , S. Safarpour , R. Drechsler , M. Abadir, Debugging sequential circuits using Boolean satisfiability, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.204-209, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382572]
• 5: Vamsi Boppana , Rajarshi Mukherjee , Jawahar Jain , Masahiro Fujita , Pradeep Bollineni, Multiple error diagnosis based on xlists, Proceedings of the 36th ACM/IEEE conference on Design automation, p.660-665, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.310021]
• 6: G. Cabodi , P. Camurati , F. Corno , S. Gai , P. Prinetto , M. Sonza Reorda, A new model for improving symbolic product machine traversal, Proceedings of the 29th ACM/IEEE conference on Design automation, p.614-619, June 08-12, 1992, Anaheim, California, United States
• 7: 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
• 8: Efficient Design Error Correction of Digital Circuits, Proceedings of the 2000 IEEE International Conference on Computer Design: VLSI in Computers & Processors, p.465, September 17-20, 2000
• 9: S.-Y. Huang and K.-T. Cheng. Errortracer: Design error diagnosis based on fault simulation techniques. IEEE Trans. on CAD, 18(9):1341--1352, 1999.
• 10: Andreas Kuehlmann , David I. Cheng , Arvind Srinivasan , David P. LaPotin, Error diagnosis for transistor-level verification, Proceedings of the 31st annual conference on Design automation, p.218-224, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196358]
• 11: T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Trans. on CAD, 11:4--15, 1992.
• 12: Chih-Chang Lin , Kuang-Chien Chen , Shih-Chieh Chang , Malgorzata Marek-Sadowska , Kwang-Ting Cheng, Logic synthesis for engineering change, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.647-652, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217604]
• 13: J. Liu and A. Veneris. Incremental fault diagnosis. IEEE Trans, on CAD, 24(4):1514--1545, 2005.
• 14: 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
• 15: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 16: A. Smith. Diagnosis of combinational logic circuits using Boolean satisfiability. Master's thesis, University of Toronto, Canada, 2004.
• 17: 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
• 18: A. Veneris and I. N. Hajj. Design error diagnosis and correction via test vector simulation. IEEE Trans. on CAD, 18(12):1803--1816, 1999.
• 19: Jesse Whittemore , Joonyoung Kim , Karem Sakallah, SATIRE: a new incremental satisfiability engine, Proceedings of the 38th conference on Design automation, p.542-545, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379019]