Debugging complex counterexample of hardware system using control flow distance metrics

We propose a novel debugging technique for complex counterexample generated by model checking complex hardware system. It searches for a witness with control flow as similar as possible to a counterexample generated by model checker. Then it performs dynamic slicing on the difference between this two control flows, to obtain the set of difference that are actually relevant to the violation of assertion. There are tightly relation between this set and the actual bug. Starting from this difference set, actual bug can then be located by perform a breath-first source code checking. Experiment result shows that our approach is highly accurate.