Formal Verification Guided Automatic Design Error Diagnosis and Correction of Complex Processors

In this paper we present a method to automatically debug and correct design errors of modern microprocessors. Given a golden sequential model of the processor and the erroneous cycle-accurate model of superscalar out-of-order processors, we employ a multiplexer-based method, which has been used for RTL/gate-level designs, to formally identify the candidate locations for the errors/bugs along with a counter example to guide the error correction mechanism. By analyzing the design and the generated candidate locations and the corresponding counter example, we automatically generate a set of potential solutions to correct the error. Finally, the potential solutions are formally verified against the golden model until the error is corrected. To show the effectiveness of our method, we have chosen a complex out-of-order superscalar processor with timing error recovery mechanisms as our case study. We have injected a number of bugs in the processor model and could successfully find the bugs and also their corresponding fixes.