SAT-based Design Debugging and Fault Localisation
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
- Design Debugging. We are given a chip design
which does not satisfy its specification, witnessed by a
- 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