Formal-Analysis-Based Trace Computation for Post-Silicon Debug

This paper presents a post-silicon debug methodology that provides a means to rewind, or backspace, a chip from a known crash state using a combination of on-chip real-time data collection and off-chip formal analysis methods. A complete debug flow is presented that considers practical considerations such as area, on-chip non-determinism and signal propagation delay. This flow, along with a low-overhead breakpoint circuit, allows for state-accurate breakpointing capabilities without the need to monitor the entire state of the chip. The flow and associated hardware was tested using a hardware prototype, which consists of an OpenRISC processor instrumented with the debug hardware connected to a PC running the formal verification algorithms. Traces hundreds of cycles long were obtained using the methodology presented in this paper.