  We present Symbolic Quick Error Detection (Symbolic QED), a structured
approach for logic bug detection and localization which can be used both during
pre-silicon design verification as well as post-silicon validation and debug.
This new methodology leverages prior work on Quick Error Detection (QED) which
has been demonstrated to drastically reduce the latency, in terms of the number
of clock cycles, of error detection following the activation of a logic (or
electrical) bug. QED works through software transformations, including
redundant execution and control flow checking, of the applied tests. Symbolic
QED combines these error-detecting QED transformations with bounded model
checking-based formal analysis to generate minimal-length bug activation traces
that detect and localize any logic bugs in the design. We demonstrate the
practicality and effectiveness of Symbolic QED using the OpenSPARC T2, a
500-million-transistor open-source multicore System-on-Chip (SoC) design, and
using "difficult" logic bug scenarios observed in various state-of-the-art
commercial multicore SoCs. Our results show that Symbolic QED: (i) is fully
automatic, unlike manual techniques in use today that can be extremely
time-consuming and expensive; (ii) requires only a few hours in contrast to
manual approaches that might take days (or even months) or formal techniques
that often take days or fail completely for large designs; and (iii) generates
counter-examples (for activating and detecting logic bugs) that are up to 6
orders of magnitude shorter than those produced by traditional techniques.
Significantly, this new approach does not require any additional hardware.
