Automated debugging of counterexamples in formal verification of pipelined microprocessors

We propose a novel method for error diagnosis of pipelined microprocessors that allows us to exploit Positive Equality in Correspondence Checking. We also present static CNF variable ordering heuristics that dramatically reduce the solution space during the debugging. Experimental results indicate speedup of up to 2 orders of magnitude relative to previous approaches when applying the method to automated debugging in formal verification of complex pipelined DSPs.