Post-Silicon Debug Using Formal Verification Waypoints

Applying formal methods to assist in the post-silicon debugging of complex digital designs presents challenges that are distinct from those found in pre-silicon formal verification. In post-silicon debug, a set of observed events or conditions describes a failure scenario. The task is to identify a reasonably general set of input and hardware state conditions that inevitably produces that failure scenario. That set of conditions may be represented in the form of a counterexample to a desired property. Modern formal verification methods are especially adept at finding counterexamples to properties, and can often do so efficiently in large state spaces. This paper describes a method of assisting the discovery of counterexamples using user- hypothesized preconditions, or waypoints, of the failure. Each waypoint is an event that is believed to occur prior to the observed failure of the target property. By guiding formal analysis through a sequence of waypoints, the time required to find a counterexample of the target property can be significantly reduced. A specific case study is presented to illustrate the application and performance of our method using an actual example from the post-silicon debug of a 33-million-gate chip. I. INTRODUCTION