Title :
BackSpace: Formal Analysis for Post-Silicon Debug
Author :
De Paula, Flavio M. ; Gort, Marcel ; Hu, Alan J. ; Wilton, Steven J E ; Yang, Jin
Author_Institution :
Dept. of Comput. Sci., Univ. of British Columbia, Vancouver, BC
Abstract :
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. Our preliminary simulation experiments demonstrate the potential of our approach: we can "backspace" hundreds of cycles from randomly selected states of some sample designs. Our preliminary architectural studies propose some possible implementations and show that the on-chip overhead can be reasonable. We conclude by surveying future research directions.
Keywords :
formal verification; integrated circuit design; integrated circuit testing; BackSpace; design error; formal analysis; on-chip hardware support; postsilicon debug; Circuit testing; Computer crashes; Debugging; Design engineering; Formal verification; Job shop scheduling; Monitoring; Observability; Silicon; Vehicle crash testing;
Conference_Titel :
Formal Methods in Computer-Aided Design, 2008. FMCAD '08
Conference_Location :
Portland, OR
Print_ISBN :
978-1-4244-2735-2
Electronic_ISBN :
978-1-4244-2736-9
DOI :
10.1109/FMCAD.2008.ECP.9