Automatic rectification of design errors in complex processors with programmable hardware

In this paper, we address the problem of automatic correction of design errors in microprocessors, when the correction function is implemented in lookup tables. The formal specification of an erroneous processor and its reference instruction-set architecture (ISA) model are used in an iterative process, employing formal methods, to find and fix the bugs. Then, the correction function is optimized to reduce the lookup table size. We have shown the effectiveness of our method by correcting the bugs in two complex out-of-order superscalar processors with two different timing error recovery mechanisms.