Microprocessor verification/debugging in abstracted level and their application to post-silicon debugging

Pipelined microprocessors, especially with superscalar and out-of- order mechanisms, are difficult to be formally verified mainly because they have so many different control sequences to be examined. On the other hand, in order to make microprocessors more reliable and generating higher performance, various error recovery algorithms, such as recovery from timing errors, are now incorporated on top of the highly complicated control sequences. This gives another complexity to the verification of microprocessors. The state-of-the-art formal verification techniques for high performance microprocessors analyze their behaviors in highly abstracted level in order to reduce the complexity. In this talk, first we give an improved formal verification techniques for superscalar out-of-order microprocessors with timing error recovery mechanisms. Then we introduce a debugging method for such microprocessors by inserting multiplexers in pipeline controls. These multiplexers make it possible to examine the alternative behaviors of the controllers and help in identifying portions to be modified for debugging. This is basically the same ideas which has been developed for RTL/gate designs, but here multiplexers are inserted in to the abstracted designs/models. We picked up a superscalar out-of-order processor design of reasonable size and inserted timing error recovery mechanisms by ourselves. The resulting processor design has been verified and debugged by the proposed method. The proposed method has actually identified several bugs and their locations. Based on these information, the bugs have been corrected. Although the processor design has become correct, it is implementing a subset of the instructions of the target processor, since formal verification need such reductions of designs. Real designs must be in RTL/gate and implement all instructions and mechanisms. In that sense, real designs are functionally different from their abstracted ones. Therefore, guaranteeing the correctness of real designs is another challenge and may not be complete even if their abstracted has been completely and formally verified. So we propose an approach that inserts programmable circuits into the portions of the real designs which correspond to the buggy portions in their abstracted designs. This is based on the assumptions that similar bugs that have happened in abstracted may happen again in real designs. In order to efficiently use programmable circuits, based on the actual bugs happened in abstracted designs are grouped and expanded to cover most of similar bugs. Then multiplexer based debugging method is applied to precisely identify the portions of the abstracted designs where programmable circuits should be inserted. In order to locate the corresponding portions in real designs, a simulation based signature based method is developed. By having programmable devices, similar bugs in real designs to the ones happened in abstracted designs can be rectified under post-silicon environments. We show some experimental results on how bugs in abstracted designs can be grouped and expanded to cover more bugs.