« zurück

Kolloquium | Microprocessor Verification/Debugging in Abstracted Level and their Application to Post-silicon Debugging

10.09.10 | 15:00 Uhr c.t. | Rotunde Cartsium

Masahiro Fujita | VLSI Design and Education Center | University of Tokyo

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.

In this talk, first we give an improved formal verification technique for superscalar out-of-order microprocessors with timing error recovery mechanisms. Then we introduce a debugging method for such microprocessors. Although the abstract processor design is verified, it is implementing a subset of the instructions of the target processor, since formal verification needs 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 version 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. A multiplexer based debugging method is applied to precisely identify the portions of the abstracted designs where programmable circuits should be inserted. 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. degree in Information Engineering from the University of Tokyo in 1985 and shortly after joined Fujitsu Laboratories Ltd. From 1993 to 2000, he had been assigned to Fujitsu's US research office and directed the CAD research and development group. In March 2000, he joined the department of Electronic Engineering in the University of Tokyo as a professor. He is now a professor at VLSI Design and Education Center (VDEC) in the university. He has co-authored 7 books, and has over 150 publications. He has received several awards from Japanese major scientific societies on his works in formal verification and logic synthesis. His doctor degree thesis was written in early 80's and on model checking. Since then he has been involved in many research projects on various aspects of formal verification. His current research interests include synthesis and verification in higher level design stages, hardware/software co-designs and also digital/analog co-designs.