SAT-based speedpath debugging using X traces

Due to timing variations induced by process variations and environmental effects, speedpath debugging becomes a major concern in the design of high performance VLSI circuits. In this paper, we propose an efficient approach to speedpath debugging based on Boolean Satisfiability (SAT). We use a time-discrete model of the circuit for analyzing effects of delays within the circuit. For efficiency we overapproximate sensitized paths using advanced techniques from formal hardware verification. Our approach achieves 88% decrease in the size of the debug instance leading to 71% decrease in the debugging time compared to previous work. At the same time, our new approach achieves a high diagnosis accuracy.