EE380 Computer Systems Colloquium

QED and Symbolic QED: Dramatic Improvements in SoC Validation and Debug
Wednesday, February 17, 2016 - 4:30pm to 5:30pm
Gates B03
Prof. Subhasish Mitra (Stanford) and Prof. Clark Barrett (NYU)
Abstract / Description: 

Ensuring the correctness of integrated circuits (ICs) is essential for ensuring correctness, safety and security of electronic systems we rely on. As ICs continue to grow in size and complexity, the cost and effort required to validate them are growing at an unsustainable rate. To make matters worse, difficult bugs escape into post-silicon and even production systems.

We present the Quick Error Detection (QED) technique which targets post-silicon validation and debug challenges. QED 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. Inspired by QED, we also present Symbolic QED which uses a formal engine to detect and localize bugs during both pre- and post-silicon validation.

Experimental results collected using several state-of-the-art commercial hardware platforms, as well as results obtained from from simulations of various difficult bug scenarios that occurred in commercial multi-core System-on-Chips (SoCs), demonstrate the effectiveness and practicality of QED and Symbolic QED:

Reduction in error detection latencies of up to 9 orders of magnitude, from billions of clock cycles to very few clock cycles.
Up to 4-fold improvement in bug coverage.
For an open-source industrial multi-core SoC consisting of approximately half-a-billion transistors, difficult logic bugs can be localized in only a few hours. In contrast, it might take days or weeks (or even months) of manual work (per bug) when traditional techniques are used.


The Stanford EE Computer Systems Colloquium (EE380) meets on Wednesdays 4:30-5:45 throughout the academic year. Talks are given before a live audience in Room B03 in the basement of the Gates Computer Science Building on the Stanford Campus. The live talks (and the videos hosted at Stanford and on YouTube) are open to the public.


Professor Subhasish Mitra directs the Robust Systems Group in the Department of Electrical Engineering and the Department of Computer Science of Stanford University, where he is the Chambers Faculty Scholar of Engineering. Before joining Stanford, he was a Principal Engineer at Intel.

Prof. Mitra's research interests include robust systems, VLSI design, CAD, validation and test, emerging nanotechnologies, and emerging neuroscience applications. His X-Compact technique for test compression has been key to cost-effective manufacturing and high-quality testing of a vast majority of electronic systems, including numerous Intel products. X-Compact and its derivatives have been implemented in widely-used commercial Electronic Design Automation tools. He, jointly with his students and collaborators, demonstrated the first carbon nanotube computer, and it was featured on the cover of NATURE. The US NSF presented this work as a Research Highlight to the US Congress, and it also was highlighted as "an important, scientific breakthrough" by the BBC, Economist, EE Times, IEEE Spectrum, MIT Technology Review, National Public Radio, New York Times, Scientific American, Time, Wall Street Journal, Washington Post, and numerous other organizations worldwide.

Prof. Mitra's honors include the Presidential Early Career Award for Scientists and Engineers from the White House, the highest US honor for early-career outstanding scientists and engineers, the ACM SIGDA/IEEE CEDA A. Richard Newton Technical Impact Award in Electronic Design Automation, "a test of time honor" for an outstanding technical contribution, the Semiconductor Research Corporation's Technical Excellence Award, and the Intel Achievement Award, Intel's highest corporate honor. He and his students published several award-winning papers at major venues: IEEE/ACM Design Automation Conference, IEEE International Solid-State Circuits Conference, IEEE International Test Conference, IEEE Transactions on CAD, IEEE VLSI Test Symposium, Intel Design and Test Technology Conference, and the Symposium on VLSI Technology. At Stanford, he has been honored several times by graduating seniors "for being important to them during their time at Stanford."

Prof. Mitra has served on numerous conference committees and journal editorial boards. He served on DARPA's Information Science and Technology Board as an invited member. He is a Fellow of the ACM and the IEEE.

Clark Barrett is an associate professor of Computer Science at the Courant Institute of Mathematical Sciences at New York 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.