Total correctness of VLSI chips in terms of verification and testing: In this talk we discuss how we can debug or optimize portions of designs by replacing them with look up table (LUT) or uninterpreted functions (UF). With heuristics, we replace portions of designs with LUT or UF and then they are newly synthesized according to target specifications. The basic strategy is to get solutions candidates for LUT/UF based on “small” necessary conditions and then they are incrementally refined with counter examples for the current solution candidates. We discuss the techniques in several cases. The first case is to use formal equivalence checker, actually combinational equivalence checker, in order to check the correctness of the candidate solutions completely. We show that with the state-of-the-art combinational equivalence checker, we are able to rectify designs correctly for designs having tens of thousands of gates or more. In the second case, we assume no formal verifiers available. Instead, we simply assume some sorts of simulation models exist. We show that even in this situation, it is possible to rectify designs “completely” with our proposed method, that is, designs can be 100% correctly synthesized without complete specifications.
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.