Date: February 26, 2018
Time: 2:00 PM - 3:20 PM
Location: 432 Newell Drive, Gainesville, Florida, 32611
Host: UF CISE Department
Admission: This event is free and open to the public.

Towards Unification of Synthesis and Verification in Topologically Constrained Designs

Abstract: The search space is vast for logic synthesis since any number of logic gates can be connected using any topology to come up with the best possible implementation under various design constraints. In formal verification, to achieve full coverage, an n-input circuit must be checked either explicitly or implicitly using the complete set of 2n input values. If there are p possible transformations for each logic gate or subcircuit, and there are m gates or subcircuits in the design, the number of possible transformations for the design is pm. There are, however, situations when the possible circuit topologies are limited. Logic optimization methods, in general, do not change circuit topologies dramatically. Most of them are based on series of local circuit transformations.

In this talk, I will discuss formal verification of designs produced by logic synthesis where the search space is limited, and only gates or subcircuits are transformed whereas their interconnections never change. Logic synthesis with this restriction attempts to find the best possible design among the alternatives. The logic synthesis problem can be formulated as a sequence of incremental SAT problems and the complete set of test patterns can be computed to detect all possible errors in the synthesized circuit. As long as the search space is limited to the pm alternatives, the complete set of test patterns can be used for formal verification. The number of test patterns needed in this case is experimentally shown to be very small even for circuits having several hundred inputs and several thousands logic gates. This is a step towards unification of logic synthesis and formal verification since a small number of test patterns can ensure correctness of logic synthesis. I also plan to discuss its application to computing inductive invariants and architectural/high-level synthesis for multiple chips.

Biography: Masahiro Fujita is a professor in the VLSI Design and Education Center at University of Tokyo, Japan. He received his Ph.D. in Information Engineering from the University of Tokyo in 1985 for his work on model checking of hardware designs. From 1993 to 2000, he was the Director at Fujitsu Laboratories of America and headed a hardware formal verification group. He has done pioneering works in the areas of hardware verification, high-level synthesis, testing, and software verification targeting embedded software and web-based programs. He has co-authored 10 books, and more than 300 publications. He has been involved as program and steering committee member in many prestigious conferences on CAD, VLSI design, and software engineering. His current research interests include system-on-chip synthesis and verification, hardware/software co-design targeting, digital/analog co-design, and formal analysis/verification/synthesis of cyber physical systems.