Abstract
A semi-formal verification technique, which performs a brute-force compiled simulation with a sophisticated search space pruning, has been proposed and shown to be competitive with the state-of-the-art SAT-based verification techniques, espeicially for complicated logics such as hardware having various arithmetic computation units. We have enhanced this technique by using an FPGA-based hardware accelerator (a kind of FPGA emulation but targeting formal verification), and our preliminary results showed that our verifier is about 7 times faster than the original software-based semi-formal verifier running on the state-of-the-art processors. . The approach is a sort of hardware/software co-design and co-execution approach to formal verification. We demonstrate our techniques on PC with extra FPGA board implementation.
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.