An optimum algorithm for compacting error traces for efficient functional debugging

Diagnosing counterexamples with error traces has acted as one of the most critical steps in functional verification. Unfortunately, error traces are normally very lengthy such that designers need to spend considerable effort to understand them. To alleviate designers´ burden for debugging, we present a SAT-based algorithm for reducing the lengths of error traces. The algorithm performs the paradigm of binary search algorithm to halve the search space recursively. Furthermore, it applies a theorem to guarantee to gain the shortest lengths for the error traces. Experimental results demonstrate that our approach greatly surpasses previous work and indeed has the optimum solutions.