Debugging and optimizing high performance superscalar out-of-order processors using formal verification techniques

This paper proposes a multiplexer based method, which has been used for RTL/gate level debugging, into cycle accurate design of high performance microprocessors so that complicated superscalar out-of-order processors with performance optimization techniques can be formally debugged and optimized. The results show that our debugging method reduces the complexity of the counterexamples so that verification engineers can quickly locate the bugs. In addition, our optimization technique not only improves the performance of the target processor by avoiding unnecessary stalls and replays, but also reduces the complexity of the verification process by reducing the size of the formulas to be checked by SAT/SMT solvers despite the fact that the number of simulation cycles increases. The results show that the size of the propositional formulas for verification is reduced by up to an order of magnitude and also their verification time by up to two orders of magnitude has been reduced.