SAT Based Design Debugging

Propositional Satisfiability (SAT) is seeing increasing use in design verification. One usage scenario involves encoding a verification task as an instance of SAT with the formula representing erroneous conditions. Thus, verification involves proving that this instance is unsatisfiable, i.e., that there are no erroneous conditions. If this is not the case, then a satisfying assignment provides a “counter-example” which can then be used to debug the design. In an alternate use of SAT for design debugging, the specification is inconsistent with the behavior, and therefore yields an inconsistent SAT instance. There are two separate scenarios where such an inconsistency arises. In the first, you have an implementation which does not satisfy its point-wise specification (i.e., test-cases fail). In the second, you have the golden model for the implementation and the observed behavior does not adhere to it. In either scenario, the unsatisfiable SAT instance can then be diagnosed to pin-point the fault. This diagnosis uses the notion of correction sets, which is intimately tied to the notion of unsatisfiable subsets (aka cores) and the MAX-SAT problem. In this talk, I will cover design debugging using correction sets and show its application in hardware logic design debugging, software debugging and finally silicon debugging (aka post-silicon validation). Silicon debugging poses difficult challenges due to limited design observability. I will show how the notion of the “backbone” of a satisfiable SAT instance is useful in maximizing information flow in this limited observability context.

Sharad Malik, Princeton University

Sharad Malik received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, New Delhi, India in 1985 and the M.S. and Ph.D. degrees in Computer Science from the University of California, Berkeley in 1987 and 1990 respectively. Currently he is the George Van Ness Lothrop Professor of Engineering and Electrical Engineering at Princeton University.

His research focuses on design methodology and design automation for computing systems. He is the Director of the FCRP Gigascale Systems Research Center, a multi-university effort directed towards addressing chip/package-scale system design challenges with a ten year horizon. His research in functional timing analysis and propositional satisfiability has been widely used in industrial electronic design automation tools.

He has received the NSF Young Investigator Award (1994), the CAV Award (2009, for fundamental contributions to the development of high-performance Boolean satisfiability solvers) as well as several best paper and teaching awards. He serves/has served on the program committees of leading conferences and editorial boards of leading journals. He is a fellow of the IEEE. He has published numerous papers, book chapters and a book (Static Timing Analysis for Embedded Software) describing his research.