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 will discuss how SAT solvers can be used to provide automated
support for localizing faults. My talk will address two different
scenarios: a) Design Debugging. We are given a chip design which does not satisfy it's specification, witnessed by a failing test-case. b)
Post-Silicon Validation. An observed behavior of the prototype of an
integrated circuit deviates from the 'golden model'. In both cases, we
will use a SAT solver to pin-point the temporal and spatial 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
(aka cores) and the MAX-SAT problem. Moreover, I will show how the
notion of the “backbone” of a satisfiable SAT instance is useful to
propagate information in the case where observability is limited.
Dr. Georg Weissenbacher is a postdoctoral research associate at
Princeton University. His research interests include automated
software and hardware verification, fault localization, and decision
procedures. He received his doctorate in computer science in 2010 from Oxford University, where he was working on interpolation-based software model checking.