A succinct memory model for automated design debugging

ABSTRACT

In today's complex SoC designs, verification and debugging are becoming ever more crucial and increasingly time-consuming tasks. The prevalence of embedded memories adds to the difficulty of the problem by exponentially increasing the statespace of the design. In this work, a novel memory model for design debugging is presented. It models memory succinctly by avoiding an explicit representation for each memory bit. The method uses the simulation of the erroneous design to guide the debugging process. This results in a parameterizable formal encoding that grows linearly with the erroneous trace length, significantly reducing the memory requirements of the debugging problem. In addition, the proposed model is extended to handle an arbitrary initial memory configuration, as well as non-cycle accurate output traces where only a final expected memory state is available for comparison. Experiments on industrial designs show a 96% average reduction in memory usage along with a noticeable performance improvement compared to previous work.

REFERENCES

• 1: Prakash Rashinkar , Peter Paterson , Leena Singh, System-on-a-chip verification: methodology and techniques, Kluwer Academic Publishers, Norwell, MA, 2001
• 2: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 3: N. Amla, X. Du, A. Kuehlmann, R. Kurshan, and K. McMillan, "An analysis of SAT-based model checking techniques in an industrial environment." in CHARME, 2005, pp. 254--268.
• 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: 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.
• 6: Shi-Yu Huang , Kwant-Ting Cheng, Formal Equivalence Checking and Design DeBugging, Kluwer Academic Publishers, Norwell, MA, 1998
• 7: Niraj K. Jha , Sandeep Gupta, Testing of Digital Systems, Cambridge University Press, New York, NY, 2002
• 8: Sean Safarpour , Andreas Veneris, Abstraction and refinement techniques in automated design debugging, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
• 9: Malay K. Ganai , Aarti Gupta , Pranav Ashar, Verification of Embedded Memory Systems using Efficient Memory Modeling, Proceedings of the conference on Design, Automation and Test in Europe, p.1096-1101, March 07-11, 2005 [doi>10.1109/DATE.2005.325]
• 10: Panagiotis Manolios , Sudarshan K. Srinivasan , Daron Vroon, Automatic memory reductions for RTL model verification, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California [doi>10.1145/1233501.1233663]
• 11: T. Larrabee, "Test pattern generation using Boolean satisfiability," IEEE Trans. on CAD, vol. 11, pp. 4--15, 1992.
• 12: 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]
• 13: N. Eén and N. Sörensson, "An extensible SAT-solver," in Int'l Conf. on Theory and Applications of Satisfiability Testing, 2003, pp. 502--518.
• 14: 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
• 15: N. Eén and N. Sörensson, "Translating pseudo-boolean constraints into SAT," in JSAT, vol. 2, 2006, pp. 1--26.
• 16: OpenCores.org, "http://www.opencores.org," 2006.