Fault Diagnosis and Logic Debugging Using Boolean Satisfiability

ACAL Seminar Room 1690 CSE
2:00 – 3:30 PM Friday, January 20, 2006
North Campus, University of Michigan

By

Andreas Veneris
University of Toronto
Department of Computer Science

Abstract: Recent years have seen an increased use of Boolean satisfiability (SAT) in the design cycle for Very Large Scale Integration (VLSI) circuits as an engine to solve intractable problems. The use of SAT in the VLSI design cycle is strengthened by the amount of ongoing research into SAT solvers. Any improvement to the state-of-the-art in SAT solving immediately benefits all SAT-based solutions. Although useful in many stages of the design cycle, logic diagnosis has not been addressed within a satisfiability-based framework. Logic diagnosis arises in the digital VLSI cycle during logic debugging and during failure analysis for a defective chip. In this talk we will present the first Boolean SAT-based formulation for multiple fault diagnosis and multiple design error diagnosis in combinational and sequential circuits. A number of heuristics will be outlined that improve performane for large designs. We will conclude with a QBF-based SAT formulation for the problem of diagnosis that allows for debugging of large industrial designs in a memory efficient manner. An extensive suite of experiments on large benchmark and industrial circuits corrupted with different types of faults and errors will be presented to confirm its robustness and practicality. These results suggest that satisfiability captures significant characteristics of the problem of diagnosis and they encourage novel research in satisfiability-based diagnosis approaches as a complementary process to this of design verification.

VITA: Andreas Veneris received the Diploma in Computer Engineering and Informatics from the University of Patras in 1991, the M.S. degree in Computer Science from the University of Southern California, Los Angeles in 1992 and the Ph.D. degree in Computer Science from the University of Illinois at Urbana-Champaign in 1998. He currently is an Associate Professor cross-appointed with the Department of Electrical and Computer Engineering and the Department of Computer Science at the University of Toronto. His research interests include algorithms and CAD tools for test, verification and synthesis of digital systems and circuits. He is co-recipient of a best paper award in ASP-DAC'01, co-author of a book and member ofIEEE, ACM, AAAS, Technical Chamber of Greece and The Planetary Society. He was alsoco-founder of a start-up company in 1994 that performed the first webcasting ever for the 37th Annual Grammy Awards.