Fault Localization and Correction with QBF

摘要

In this paper, we study the use of QBF solvers for fault localization and correction of sequential circuits. Given a violated specification, we compute whether the circuit can be repaired by evaluating a sequence of quantified Boolean formulas. If a repair exists, it can be extracted from a certificate for another quantified Boolean formula. Because it only finds components when a repair is possible, this approach is more precise than a satisfiability-based approach that we have developed earlier. We demonstrate this in an experimental evaluation.