Speaker: Clark Barrett
Seminar: CITRIS People and Robots Initiative, “Design of Robotics and Embedded systems, Analysis, and Modeling” Seminars (DREAMS) | Monday, March 06 | 4 – 5 PM | 250 Sutardja Dai Hall | Webcast
Quick error detection (QED) is an existing technique that transforms existing SoC test suites to improve coverage and reduce error detection latency. I will discuss two recent results which use formal methods to greatly enhance the power of QED. First, Symbolic QED is a method which uses bounded model checking to exhaustively search for short sequences of instructions which could cause QED checks to fail. Symbolic QED finds logic bugs and is applicable both to pre- and post-silicon designs. Second, Electrical QED is a technique that uses a small amount of additional hardware coupled with bounded model checking and QED to quickly localize post-silicon electrical bugs to specific design blocks and even to a handful of flip-flops within those design blocks. Both techniques were evaluated on the OpenSPARC T2 SoC with a wide variety of injected logic and electrical bugs. The new techniques automatically found and localized the injected bugs.
_______________________________________________________________
Clark Barrett is an Associate Professor (Research) of Computer Science at Stanford University, with expertise in constraint solving and its applications to verification. His Ph.D 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.