• Welcome
• Mission and Vision
• Research Interests
• Publications
• Research Projects
  • Post-Silicon Debug
  • Abstraction-Guided Simulation
  • Parallel & Distributed Model Checking

BackSpace

Post-silicon debug is the problem of determining what's wrong when the fabricated chip of a new design behaves incorrectly. This problem now consumes over half of the overall verification effort on large designs, and the problem is growing worse. We introduce a new paradigm for using formal analysis, augmented with some on-chip hardware support, to automatically compute error traces that lead to an observed buggy state, thereby greatly simplifying the post-silicon debug problem. BackSpace allows the chip to run at full speed, but then provides the effect of being able to run backwards (hence, its name) from a crash or observed bug, computing a trace of exactly what led up to the problem.

BackSpace Toolkit

Release v0.3 (Last updated on May-05-2010)

You may want to read this version's Release Notes and License - (lgpl.txt).

Also, I'm releasing both TAB-BackSpace and nuTAB-BackSpace tools by demand only. E-mail me if you want the their source files.

BackSpace Literature

NOTE: These are local copies. Originals are available from IEEE.

nuTAB-BackSpace: Rewriting to Normalize Non-Determinism in Post-Silicon Debug Traces, Flavio M. de Paula, Alan J. Hu, Amir Nahir. To Appear at Computer Aided Verification (CAV'12), USA [bibtex]

Lazy Suspect-Set Computation: Fault Diagnosis for Deep Electrical Bugs, Dipanjan Sengupta, Flavio M. de Paula, Alan J. Hu, Andre Ivanov, Andreas Veneris. In Proceeding of the Great Lakes Very Large Scale Integration Conference (GLVLSI'12), USA [bibtex]

TAB-BackSpace: Unlimited-length trace buffers with zero additional on-chip overhead, Flavio M. de Paula, Amir Nahir, Ziv Nevo, Avigail Orni, Alan J. Hu. Design Automation Conference (DAC'11), USA [bibtex]

Formal-Analysis-Based Trace Computation for Post-Silicon Debug Gort, M., De Paula, F. M., Kuan, J. J. W., Aamodt, T. M., Hu, A. J., Wilton, S. J. E., Yang, J. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. PP, issue 99, pp. 1-14, year 2011 [bibtex]

Accelerating Trace Computation in Post-Silicon Debug Johnny Kuan, Steve J. E. Wilton, Tor M. Aamodt. IEEE International Symposium on Quality Electronic Design (ISQED 2010), pp. 244-249, USA [bibtex]

BackSpace: Moving Towards Reality, Flavio M. de Paula, Marcel Gort,Alan J. Hu, Steve Wilton. Microprocessor Test and Verification (MTV'08), USA [bibtex]

BackSpace: Formal Analysis for Post-Silicon Debug, Flavio M. de Paula, Marcel Gort, Alan J. Hu, Steve Wilton, Jin Yang. Formal Methods in Computer Aided Design (FMCAD'08), USA [bibtex]