| Boolean satisfiability (SAT) solvers are being used to solve an increasing number of Electronic Design Automation (EDA) problems. This trend is largely due to significant advances in SAT solving algorithms in recent years. SAT has already been shown to be a powerful and flexible tool for solving many existing EDA problems. However, no SAT-based solution has yet been proposed for the problem of diagnosis. This thesis presents a novel SAT-based framework for performing diagnosis of combinational logic circuits. An algorithm is described which can be used for model-free design error and fault diagnosis, and for model-based fault diagnosis using several common fault models. Several heuristics are analysed that improve the runtime and reduce the memory requirements of the algorithm. |
