Date	September 21, 2017
Speaker	Clark Barrett Stanford University
Title	Dramatic Improvements in Pre-silicon and Post-silicon Validation of Digital Systems with Quick Error Detection and Formal Methods
Abstract	Ensuring the correctness of integrated circuits (ICs) is essential for ensuring the correctness, safety and security of the many electronic systems we rely on. However, the effort required to validate ICs continues to be a major bottleneck in modern system design. To make matters worse, difficult bugs still escape into post-silicon and even production systems. I will present a set of results based on Quick Error Detection (QED). The standard QED technique is a testing technique which drastically reduces error detection latency, the time elapsed between the occurrence of an error caused by a bug and its manifestation as an observable failure. I will then present two new techniques, Symbolic QED and Electrical QED which use formal methods to dramatically extend the reach of QED: to automatically detect and localize both logic and electrical bugs during both pre- and post-silicon validation. Experimental results collected from several commercial designs as well as hardware platforms demonstrate the effectiveness and practicality of these methods. For example, for a 500 million transistor multi-core IC, Symbolic QED automatically detected and localized difficult logic design bugs (the kind that could escape traditional simulation-based pre-silicon verification) in only a few hours (~ 8 hours on average). This research was performed at Stanford University in collaboration with Prof. Subhasish Mitra, several graduate students, and several industrial collaborators.
Bio	Clark Barrett is an associate professor (research) of computer science at Stanford University, with expertise in constraint solving and its applications to verification. His PhD dissertation introduced a novel approach to constraint solving now known as satisfiability modulo theories (SMT). His subsequent work on SMT has been recognized with a best paper award at DAC, an IBM Software Quality Innovation award, the Haifa Verification Conference award, and first-place honors at the SMT, CASC, and SyGuS competitions. He was also an early pioneer in the development of formal hardware verification: at Intel, he collaborated on a novel theorem prover used to verify key microprocessor properties; and at 0-in Design Automation (now part of Mentor Graphics), he helped build one of the first industrially successful assertion-based verification tool-sets for hardware.
Resources