The latest advancements in the commercial formal model checkers have enabled the integration of formal property verification with the conventional testbench based methods in the overall verification plan. This has led to significant verification productivity across the entire design flow (from architectural verification to post-silicon debugging). As verification productivity is improved, debugging efficiency has become more important than before. In this paper, we discuss how formal technology can be leveraged to bring efficiency in the debugging process. In particular, we discuss how "behavioral indexing" enables a top-down view of the counter-example and facilitates debugging by overlaying a higher abstraction view on the bit-level counter-example. We also discuss how formal technology can be leveraged to do "what-if" analysis to localize the root cause of the bug. We also discuss how formal technology supports the even more challenging task of traceless debugging (the process of debugging the "absence of witness/counter-example").