“SAT-based Design Debugging and Its Application to Undergraduate Circuit Experiment”

Name: Takeshi Matsumoto
Date and Time: Friday, September 7 at 11:00 a.m. – 12:00 p.m.

Location: Donald Bren Hall 3011

Abstract:

As VLSI designs are becoming larger and more complicated, designers spend a larger amount of
time for verification and debug to detect bugs in designs and avoid them. Moreover, some bugs may not be detected in the verification processes before fabrication and are only recognized by running an actual chip after fabrication. In post-silicon debugging, it is not practical that a large part of the circuit is changed for fixing bugs, since such large change requires designers to do time-consuming physical and timing design processes again. Usually, more than a half of the verification time is spent for correcting the buggy portions of the designs rather than identifying them, since debugging is much less automated than checking correctness of the designs. Thus, automating and shortening the debugging processes is now one of the most important issues in VLSI designs. In this talk, SAT-based design debugging methods in gate-level and behavior-level are introduced. In the methods, debugging consists of two processes: locating the suspicious portions in the designs and correcting them through replacements with appropriate sets of gates. In the locating process, designers try to find locations of bugs (or candidate locations) which should be the root cause of the bugs. Then, they modify logic functions at those possibly buggy locations in the correcting process. Both processes can be solved by repeatedly solving Boolean satisfiability (SAT) problems by introducing programmable logic elements, such as MUX (multiplexer) and/or LUT (look-up table), to the original designs under debugging. This talk gives the details of the theoretical aspect of those methods and experimental results on several circuits. In the last part of the talk, a trial activity to apply the debugging methods to an undergraduate experiment, where a simple 4-bit CPU is made on breadboard through six 90-minute classes, is introduced.
This activity can be seen as an application example of state-of-the-art research results to education field.

Biography:

Takeshi Matsumoto is an Associate Professor in the Department of Electronics and Information
Engineering at National Institute of Technology, Ishikawa College, Japan. He directs Integrated System Lab in the department. He received his M.S. and Ph.D. degrees in Electronic Engineering from the University of Tokyo, Japan, in 2005 and 2008, respectively. The topic of his Ph.D. thesis is equivalence checking of system level design. From 2008 to 2013, he has been a Research Associate of VLSI Design and Education Center, the University of Tokyo. His research interests include formal verification of system-level designs, automated debugging and debugging support for pre- and post-silicon circuits, education and teaching materials on electric and electronic circuits. He received IPSJ Yamashita SIG Research Award in 2012 from Information Processing Society of Japan.