Design diagnosis using Boolean satisfiability
Alexander D. S. Smith, Andreas G. Veneris, Anastasios Viglas · 2004
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. This paper attempts 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. 1