Managing complexity in design debugging with sequential abstraction and refinement

Design debugging is becoming an increasingly difficult task in the VLSI design flow with the growing size of modern designs and their error traces. In this work, a novel abstraction and refinement technique for design debugging is presented that addresses two key components of the debugging complexity, the design size and the error trace length. The abstraction technique works by under-approximating the debugging problem by removing modules of the original design and replacing them with simulated values of the erroneous circuit. After each abstract problem is solved, the refinement strategy uses the resulting UNSAT core to direct which modules should be refined. This refinement strategy is extended by allowing refinement of across time-frames in addition to modules. Experimental results show that the proposed algorithm is able to return solutions for all instances compared to only 41% without the technique demonstrating the viability of this approach in tackling real-world debugging problems.