Exact Diagnosis Using Boolean Satisfiability

We propose an exact algorithm to model-free diagnosis with an application to fault localization in digital circuits. We assume that a faulty circuit and a correctness specification, e.g., in terms of an un-optimized reference circuit, are available. Our algorithm computes the exact set of all minimal diagnoses up to cardinality k considering all possible assignments to the primary inputs of the circuit. This exact diagnosis problem can be naturally formulated and solved using an oracle for Quantified Boolean Satisfiability (QSAT). Our algorithm uses Boolean Satisfiability (SAT) instead to compute the exact result more efficiently. We implemented the approach and present experimental results for determining fault candidates of digital circuits with seeded faults on the gate level. The experiments show that the presented SAT-based approach outperforms state-of-the-art techniques from solving instances of the QSAT problem by several orders of magnitude while having the same accuracy. Moreover, in contrast to QSAT, the SAT-based algorithm has any-time behavior, i.e., at any-time of the computation, an approximation of the exact result is available that can be used as a starting point for debugging. The result improves while time progresses until eventually the exact result is obtained.