Post-silicon validation and debug using symbolic quick error detection

Patent metadata

Field	Value
Publication number	US-10528448-B2
Application number	US-201615577065-A
Country	US
Kind code	B2
Filing date	Jun 6, 2016
Priority date	Jun 6, 2015
Publication date	Jan 7, 2020
Grant date	Jan 7, 2020

Abstract

Disclosed are improved methods and structures for verifying integrated circuits and in particular systems-on-a-chip constructed therefrom. We call methods and structures according to the present disclosure Symbolic Quick Error Detection or Symbolic QED, Illustrative characteristics of Symbolic QED include: 1) It is applicable to any System-on-Chip (SoC) design as long as it contains at least one programmable processor; 2) It is broadly applicable for logic bugs inside processor cores, accelerators, and uncore components; 3) It does not require failure reproduction; 4) It does not require human intervention during bug localization; 5) It does not require trace buffers, 6) It does not require assertions; and 7) It uses hardware structures called “change detectors” which introduce only a small area overhead. Symbolic QED exhibits: 1) A systematic (and automated) approach to inserting “change detectors” during a design phase; 2) Quick Error Detection (QED) tests that detect bugs with short error detection latencies and high coverage; and 3) Formal techniques that enable bug localization and generation of minimal bug traces upon bug detection.

First claim

The invention claimed is:

1. A computer implemented method for the post-silicon validation and debug of a digital hardware system comprising the steps of:
inserting, automatically and systematically a number of change detectors into the digital hardware system during a design phase of that hardware system;
running, a number of quick error detection (QED) tests on that hardware system having the inserted change detectors wherein the change detectors record debug information during the running;
determining, whether an error (bug) was detected by the QED tests; and
if a bug was detected by the QED tests then localizing the detected bug and generating a minimal bug trace through the use of a formal analysis; and
outputting a set of candidate location(s) for each detected bug and the minimal bug trace(s).

2. The computer implemented method of claim 1 wherein the digital system is a System on a Chip (SoC) having at least one programmable processor.

3. The computer implemented method of claim 2 further comprising:
stopping the system when QED test(s) detects an error;
saving any change detector value(s); and
using the saved change detector value(s), generating a reduced design for further analysis;
wherein the reduced design excludes any components from BMC analysis if, during a change window, change detector(s) associated with those components did not record any changes in the logic values of the components input or output signals.

4. The computer implemented method of claim 1 wherein the formal analysis employs bounded model checking (BMC) methodology.

5. The computer implemented method according to claim 4 comprising ensuring that only QED-compatible bug traces are considered by BMC by adding a new QED module to a fetch stage of each processor core during BMC.

6. The computer implemented method according to claim 5 wherein the QED module automatically transforms a sequence of original instructions into a QED-compatible sequence.

7. The computer implemented method according to claim 6 further comprising establishing a QED-consistent state before starting the BMC.

8. The computer implemented method of claim 7 wherein the change detectors are inserted at boundaries of all components that may potentially be removed during a further analysis.

9. The computer implemented method of claim 1 wherein the QED employs a number of QED transformations selected from the group consisting of Error Detection using Duplicated Instructions for Validation (EDDI-V) and Proactive Load and Check (PLC) transformations.

10. The computer implemented method of claim 1 wherein the change detectors include a k-bit ripple counter that is initialized to all 1's and is reset to all 0's whenever a change in signal value is detected.

Assignees

• Univ Leland Stanford Junior
• Univ New York

Inventors

• Mitra Subhasish
• Barrett Clark
• Lin David
• Singh Eshan

Classifications

• G06F11/3466 Primary

  Performance evaluation by tracing or monitoring · CPC title

• G06F11/3079

  the data filtering being achieved by reporting only the changes of the monitored data · CPC title

• G06F11/3003

  Monitoring arrangements specially adapted to the computing system or computing system component being monitored · CPC title

• G06F11/2236

  to test CPU or processors · CPC title

• G06F11/3024

  where the computing system component is a central processing unit [CPU] · CPC title