Using QBF to increase accuracy of SAT-based debugging

Debugging significantly slows down the design process of complex systems. Only limited tool support is available and often fixing one problem leads to finding the next one. Here, we propose an approach that integrates formal verification with diagnosis. The approach is based on Quantified Boolean Formulas (QBF) and ensures, that counterexamples of high quality are returned. Moreover, the diagnosis algorithm only returns fault candidates that can fix all counterexamples. By this, the total number of fault candidates decreases and less iterations between verification and debugging are required.