Design diagnosis using Boolean satisfiability

Recent advances in Boolean satisfiability have made it an attractive engine for solving many digital VLSI design problems such as verification, model checking, optimization 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 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.