Prof. Masahiro Fujita
VLSI Design and Education Center The University of Tokyo
Title: Unified logic framework for synthesis, testing and diagnosis

Abstract: In this talk, we first show QBF (Quantified Boolean Function) based partial logic synthesis methods which can fill the vacant subcircuits in the given designs in such a way that the overall circuits become correct or the ones as intended. When generating the functions for the subcircuits, incoming signals to the subcircuits are not allowed to change. Due to this restriction, the QBF problems for the partial logic synthesis can be solved efficiently. The partial synthesis can be made with or without logic specification. If no logic specification is available, the partial synthesis methods try to generate unique functions for the vacant subcircuits. In the second part we show that the partial logic synthesis methods can also be applied to logic debugging, ECO (Engineering Change Order), and automatic test pattern generation and diagnosis for various multiple faults.

Various experimental results are given on these problems. In the last part of the talk, the partial logic synthesis is extended to allow to change the incoming signals to the subcircuits. This is achieved by a new formulation of the problem and makes it possible for partial logic synthesis to dynamically change the connections in the given designs. Hence the partial logic synthesis can be much more powerful in terms of circuit restructuring.

Biography: Masahiro Fujita received his Ph.D. in Information Engineering from the University of Tokyo in 1985 on his work on model checking of hardware designs by using logic programming languages. In 1985, he joined Fujitsu as a researcher and started to work on hardware automatic synthesis as well as formal verification methods and tools, including enhancements of BDD/SAT-based techniques. From 1993 to 2000, he was director at Fujitsu Laboratories of America and headed a hardware formal verification group developing a formal verifier for real-life designs having more than several million gates. The developed tool has been used in production internally at Fujitsu and externally as well. Since March 2000, he has been a professor at VLSI Design and Education Center of the University of Tokyo. He has done innovative work in the areas of hardware verification, synthesis, testing, and software verification-mostly targeting embedded software and web-based programs. He has been involved in a Japanese governmental research project for dependable system designs and has developed a formal verifier for C programs that could be used for both hardware and embedded software designs. The tool is now under evaluation jointly with industry under governmental support. He has authored and co-authored 10 books, and has more than 200 publications. He has been involved as program and steering committee member in many prestigious conferences on CAD, VLSI designs, software engineering, and more. His current research interests include synthesis and verification in SoC (System on Chip), hardware/software co-designs targeting embedded systems, digital/analog co-designs, and formal analysis, verification, and synthesis of web-based programs and embedded programs.