|
| |
|
| During post-silicon debug, formal verification is viewed as important to rapidly validate fixes, as well as to isolate the root cause for silicon bugs, and prevent expensive serial bugs where the debug team is iterating and iterating in a loop without the proper root cause analysis. |
|
|
|
|
| Often, problems in silicon are hard to reproduce in simulation and extra effort is spent in trial and error methods of capturing the right input sequence. Formal technology can quickly eliminate incorrect hypotheses and is capable of locating the root cause of the bug. By appropriately leveraging formal technology, along with simulation methods of post-silicon debugging, the entire process can be expedited. Once the bug is root caused and appropriate fix is made, formal technology can establish that the fix indeed eliminates the problem and has not introduced any new design error. |
| |
- Isolate the root cause for silicon bugs: In many post-silicon debug situations, the team has some ability to extract a trace of what went wrong in the chip when it failed, but this trace is often severely limited. So the team is in the situation that they can identify some wrong behavior at the output of the chip, but do not understand the triggering event for this incorrect behavior. With formal technology, the process of isolating the root cause for the silicon bug is much more predictable than simulation, because of the capability to find counter-examples very rapidly.
- Prevent expensive serial bugs: Debug teams may iterate endlessly in a loop, without proper root cause analysis. Validation of bug fixes is critical, since attempting to cure the symptom without understanding the root cause leads only to another, similar bug in the silicon respin. Formal verification, with its exhaustive nature, is well-suited to validate a fix and make sure no other corner case will trigger a similar failure.
- Rapidly validate fixes: A silicon bug may be fixed in many ways, sometimes without a respin. Yet, it is tedious and difficult to explore the effect of a proposed fix in simulation. Using formal verification, a fix can be validated quickly, due to the exhaustiveness of the technology. For example, it may confirm that a software fix is possible by limiting the number of outstanding transactions to a smaller limit, regardless of the operation conditions. (Simulation can only indicate the lack of a failure for the current trace.)
|
|
|
|
|
|
