Logic Bug Detection and Localization Using Symbolic Quick Error Detection

TL;DR

This paper introduces Symbolic QED, a formal method combining software transformations and model checking to efficiently detect and localize logic bugs in complex SoC designs, significantly reducing analysis time and bug trace length.

Contribution

It presents a fully automatic, formal approach that improves bug detection and localization speed and accuracy without additional hardware, applicable to large-scale multicore chips.

Findings

Detects and localizes logic bugs in large SoCs effectively

Reduces bug activation trace length by up to 6 orders of magnitude

Requires only a few hours for analysis, unlike manual or traditional formal methods

Abstract

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.