|SAT-based Design Debugging and Fault Localisation|
|presented at the Center for Embedded Systems for Critical Applications|
Contemporary Boolean Satisfiability (SAT) solvers are the enabling technology underlying many successful hardware verification tools. A particular strength of such tools is the detection of bugs. Discovering a bug, however, is only the first step; locating and understanding its cause is often a much more daunting task. I discuss how SAT solvers can be used to provide automated support for localising faults. My talk addresses two different scenarios:
- Design Debugging. We are given a chip design which does not satisfy its specification, witnessed by a failing test-case.
- Post-Silicon Validation. An observed behavior of the prototype of an integrated circuit deviates from the 'golden model'.