Fault diagnosis and logic debugging using Boolean satisfiability

Recent advances in Boolean satisfiability have made it attractive to solve many digital VLSI design problems such as verification and test generation. Fault diagnosis and logic debugging have not been addressed by existing satisfiability-based solutions. We attempt to bridge this gap by proposing a model-free satisfiability-based solution to these problems. The proposed formulation is intuitive and easy to implement. It shows that satisfiability captures significant problem characteristics and it offers different trade-offs. It also provides new opportunities for satisfiability-based diagnosis tools and diagnosis-specific satisfiability algorithms. Theory and experiments validate the claims and demonstrate its potential.