SAT Based Design Debugging

_
Propositional Satisfiability (SAT) is seeing increasing use in design verification. One usage scenario involves encoding a verification task as an instance of SAT with the formula representing erroneous conditions. Thus, verification involves proving that this instance is unsatisfiable, i.e., that there are no erroneous conditions. If this is not the case, then a satisfying assignment provides a “counter-example” which can then be used to debug the design. In an alternate use of SAT for design debugging, the specification is inconsistent with the behavior, and therefore yields an inconsistent SAT instance. There are two separate scenarios where such an inconsistency arises. In the first, you have an implementation which does not satisfy its point-wise specification (i.e., test-cases fail). In the second, you have the golden model for the implementation and the observed behavior does not adhere to it. In either scenario, the unsatisfiable SAT instance can then be diagnosed to pin-point the fault. This diagnosis uses the notion of correction sets, which is intimately tied to the notion of unsatisfiable subsets (aka cores) and the MAX-SAT problem. In this talk, I will cover design debugging using correction sets and show its application in hardware logic design debugging, software debugging and finally silicon debugging (aka post-silicon validation). Silicon debugging poses difficult challenges due to limited design observability. I will show how the notion of the “backbone” of a satisfiable SAT instance is useful in maximizing information flow in this limited observability context.
_

Sharad Malik, Princeton University

put your bio here