Automatic discovery and localization of tough bugs in large SoCs using formal-enhanced quick error detection

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.

Speaker: Clark Barrett, Google & Stanford Univ.