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'.

In both cases, we use a SAT solver to pin-point the temporal and spatial location of the causes (e.g., an erroneous expression in the first case, or a faulty gate in the second) of the discrepancy. In the second case, this task is complicated by the fact there are practical limitations to the observability of the internal signals of the chip. The diagnosis technique we deploy uses the notion of correction sets, which is intrinsically tied to the notion of unsatisfiable subsets of the clauses of the formula (also knows as cores) and the MAX-SAT problem. Moreover, I explain how the notion of the 'backbone' of a satisfiable SAT instance is useful to propagate information in the case where observability is limited.

Watch this talk on Vimeo. Browse other CESCA talks.