Using unsatisfiable cores to debug multiple design errors

ABSTRACT

Due to the increasing complexity of today's circuits a high degree of automation in the design process is mandatory. The detection of faults and design errors is supported quite well using simulation or formal verification. But locating the fault site is typically a time consuming manual task. Techniques to automate debugging and diagnosis have been proposed. Approaches based on Boolean Satisfiability (SAT) have been demonstrated to be very effective. In this work debugging on the gate level is considered. Unsatisfiable cores contained in a SAT instance for debugging are used (1) to determine all suspects, and (2) to speed-up the debugging process. In comparison to standard SAT-based debugging, the experimental results show a significant speed-up for debugging multiple faults.

REFERENCES

• 1: Kai-Hui Chang , I. L. Markov , V. Bertacco, Fixing Design Errors with Counterexamples and Resynthesis, Proceedings of the 2007 conference on Asia South Pacific design automation, p.944-949, January 23-26, 2007 [doi>10.1109/ASPDAC.2007.358111]
• 2: N. Eén and N. Sörensson. An extensible SAT solver. In SAT 2003, volume 2919 of LNCS, pages 502--518, 2004.
• 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: Evgueni Goldberg , Yakov Novikov, Verification of Proofs of Unsatisfiability for CNF Formulas, Proceedings of the conference on Design, Automation and Test in Europe, p.10886, March 03-07, 2003
• 5: 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
• 6: Jinbo Huang, MUP: a minimal unsatisfiability prover, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China [doi>10.1145/1120725.1120907]
• 7: Shi-Yu Huang, A Fading Algorithm For Sequential Fault Diagnosis, Proceedings of the Defect and Fault Tolerance in VLSI Systems, 19th IEEE International Symposium, p.139-147, October 10-13, 2004
• 8: Mark H. Liffiton , Karem A. Sakallah, Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints, Journal of Automated Reasoning, v.40 n.1, p.1-33, January 2008 [doi>10.1007/s10817-007-9084-z]
• 9: 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]
• 10: 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]
• 11: 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]
• 12: Yoonna Oh , Maher N. Mneimneh , Zaher S. Andraus , Karem A. Sakallah , Igor L. Markov, AMUSE: a minimally-unsatisfiable subformula extractor, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996710]
• 13: R Reiter, A theory of diagnosis from first principles, Artificial Intelligence, v.32 n.1, p.57-95, April 1987 [doi>10.1016/0004-3702(87)90062-2]
• 14: Ohad Shacham , Karen Yorav, On-the-fly resolve trace minimization, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California [doi>10.1145/1278480.1278630]
• 15: Ofer Shtrichman, Pruning Techniques for the SAT-Based Bounded Model Checking Problem, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.58-70, September 04-07, 2001
• 16: A. Smith, A. Veneris, M. Fahim Ali, and A.Viglas. Fault diagnosis and logic debugging using boolean satisfiability. IEEE Trans. on CAD, 24(10):1606--1621, 2005.
• 17: Sean Safarpour , Hratch Mangassarian , Andreas Veneris , Mark H. Liffiton , Karem A. Sakallah, Improved Design Debugging Using Maximum Satisfiability, Proceedings of the Formal Methods in Computer Aided Design, p.13-19, November 11-14, 2007 [doi>10.1109/FMCAD.2007.28]
• 18: S. Staber, G. Fey, R. Bloem, and R. Drechsler. Automatic fault localization for property checking. In Haifa Verification Conference, volume 4383 of LNCS, pages 50--64. Springer, 2006.
• 19: A. Veneris and I. N. Hajj. Design error diagnosis and correction via test vector simulation. IEEE Trans. on CAD, 18(12):1803--1816, 1999.
• 20: 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]
• 21: Lintao Zhang , Sharad Malik, Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications, Proceedings of the conference on Design, Automation and Test in Europe, p.10880, March 03-07, 2003

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

General Terms:
Design, Verification

Keywords:
fault localization, sat-based debugging, unsatisfiable core