Seminars

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

Masahiro Fujita, University of Tokyo

8/19/2010, 3pm, GHC-9115

Abstract

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.

Biography

Masahiro Fujita received his Ph.D. from the University of Tokyo in 1985. He is a professor in VLSI Design and Education Center (VDEC) at the University of Tokyo. Prior to joining the University of Tokyo in 2000, he was director of CAD for VLSI in Fujitsu Laboratories of America for 6 years. He has done innovative works in the areas of digital design verification, synthesis, and testing. He has co-authored 7 books, and has over 100 publications. He has been given several research awards from Japanese scientific societies. His current research interests include synthesis and verification in higher level design stages, hardware/software co-designs and also digital/analog co-designs.