2009 Formal Methods in Computer-Aided Design
2009
The VLSI CAD flow encompasses an abundance of critical NP-complete and PSPACE-complete problems.Instead of developing a dedicated algorithm for each, the trend during the last decade has been to encode them in formal languages, such as Boolean satisfiability (SAT) and quantified Boolean formulas (QBFs), and focus academic resources on improving SAT and QBF solvers.The significant progress of these solvers has validated this strategy.This dissertation contributes to the further advancement of formal techniques in CAD.Today, the verification and debugging of increasingly complex RTL designs can consume up to 70% of the VLSI design cycle.In particular, RTL debug is a manual, resource-intensive task in the industry.The first contribution of this thesis is an in-depth examination of the factors affecting the theoretical computational complexity of debugging.It is established that most variations of the debugging problem are NP-complete.Automated debugging tools return all potential error sources in the RTL, called solutions, that can explain a given failing error trace.Finding each solution requires a separate call to a