Abstraction and refinement techniques in automated design debugging

ABSTRACT

Verification is a major bottleneck in the VLSI design flow with the tasks of error detection, error localization, and error correction consuming up to 70% of the overall design effort. This work proposes a departure from conventional debugging techniques by introducing abstraction and refinement during error localization. Under this new framework, existing debugging techniques can handle large designs with long counter-examples yet remain run time and memory efficient. Experiments on benchmark and industrial designs confirm the effectiveness of the proposed framework and encourage further development of abstraction and refinement methodologies for existing debugging techniques.

REFERENCES

• 1: Prakash Rashinkar , Peter Paterson , Leena Singh, System-on-a-chip verification: methodology and techniques, Kluwer Academic Publishers, Norwell, MA, 2001
• 2: R. Drechsler, Formal Verification of Circuits. Kluwer Academic Publishers, 2000.
• 3: Y. Yang, S. Sinha, A. Veneris, and R. Brayton, "Automating Logic Rectification by Approximate SPFDs," in ASP Design Automation Conf., 2007.
• 4: D. P. Appenzeller, Formal verification of a PowerPC microprocessor, Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and Processors, p.79, October 02-04, 1995
• 5: M. Abramovici, M. Breuer, and A. Friedman, Digital Systems Testing and Testable Design. Computer Science Press, 1990.
• 6: Shi-Yu Huang , Kwant-Ting Cheng, Formal Equivalence Checking and Design DeBugging, Kluwer Academic Publishers, Norwell, MA, 1998
• 7: A. Smith, A. Veneris, M. F. Ali, and A. Viglas, "Fault diagnosis and logic debugging using Boolean satisfiability," IEEE Trans. on CAD, vol. 24, no. 10, pp. 1606--1621, 2005.
• 8: 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
• 9: Yirng-An Chen , Fang-Sung Chen, Algorithms for compacting error traces, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan [doi>10.1145/1119772.1119792]
• 10: Kai-hui Chang , V. Bertacco , I. L. Markov, Simulation-based bug trace minimization with BMC-based refinement, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1045-1051, November 06-10, 2005, San Jose, CA
• 11: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
• 12: E. Clarke, A. Gupta, and O. Strichman, "SAT-based counterexample-guided abstraction refinement," IEEE Trans. on CAD, vol. 22, no. 7, pp. 1113--1123, 2004.
• 13: Per Bjesse , James Kukula, Using Counter Example Guided Abstraction Refinement to Find Complex Bugs, Proceedings of the conference on Design, automation and test in Europe, p.10156, February 16-20, 2004
• 14: OpenCores.org, "http://www.opencores.org," 2006.
• 15: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990