Logic Bug Detection and Localization Using Symbolic Quick Error Detection

Logic Bug Detection and Localization Using Symbolic Quick Error Detection” by Eshan Singh, David Lin, Clark Barrett, and Subhasish Mitra. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018, IEEE.

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.

Keywords: Bounded Model Checking, Debug, Formal Debugging, Post-Silicon, Validation and Debug, Quick Error Detection, QED, Symbolic Quick Error Detection

BibTeX entry:

@article{SLB+18,
   author = {Eshan Singh and David Lin and Clark Barrett and Subhasish Mitra},
   title = {Logic Bug Detection and Localization Using Symbolic Quick
	Error Detection},
   journal = {IEEE Transactions on Computer-Aided Design of Integrated
	Circuits and Systems},
   publisher = {IEEE},
   year = {2018},
   doi = {10.1109/TCAD.2018.2834401},
   url = {http://theory.stanford.edu/~barrett/pubs/SLB+18.pdf}
}

(This webpage was created with bibtex2web.)