Browse Prior Art Database

Method and System for Efficient Error Injection Analysis leveraging Formal Verification

IP.com Disclosure Number: IPCOM000240555D
Publication Date: 2015-Feb-09
Document File: 3 page(s) / 63K

Publishing Venue

The IP.com Prior Art Database

Abstract

A methodology is presented to leverage formal verification (FV) for fault/error injection analysis in a robust industrial functional verification flow. The presented methodology improves fault injection analysis/verification productivity significantly by taking advantage of FV strengths to be able to provide complete proofs of non-sensitizability of certain errors which can then be removed from consideration in a simulation-based verification speeding it immensely as those cases are the ones which require the most analysis. Furthermore, FV can inject multiple errors all at the same time improving productivity, and can assure existence of paths from fault injected latches to error-observable points in the design.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 44% of the total text.

Page 01 of 3

Method and System for Efficient Error Injection Analysis leveraging Formal Verification

Reliability/resilience is an increasingly desirable feature on hardware design and systems to make them immune to a variety of issues such as transient circuit errors, aging, environmental variations, etc. The resilience of a design to such errors is verified/estimated by exhaustive fault injection with checking to see if the function with the inserted errors results in functional breakage, and if the errors propagate to/sensitize designated portions of the designs (error detection - e.g. designated error capture registers go high) and whether the design responds to the error condition as designed (error recovery). This is typically checked in a simulation-based functional verification testbench with systematically performing the fault injections iteratively across all of the registers in the design, and simulating until the error propagates to the error capture registers. Such a simulation-based approach suffers from several drawbacks: 1) It can be time consuming with needing to iteratively inject a single error at a time (via a stuck-at override in a latch) and checking for its propagation; 2) The checking may be incomplete and inconclusive in the event the error detection points in the design do not get activated. Formal Verification (FV) offers a powerful alternative which does not suffer from these drawbacks, though suffers from capacity challenges to be able to scale to design hierarchies (e.g. unit-level) where such an analysis is applicable.

A method and system to leverage FV for fault/error injection analysis in a robust industrial functional verification flow is presented here. The presented methodology improves fault injection analysis/verification productivity significantly by taking advantage of FV strengths to be able to provide complete proofs of non-sensitizability of certain errors which can then be removed from consideration in a simulation-based verification speeding it immensely as those cases are the ones which require the most analysis. Furthermore, FV can inject multiple errors all at the same time improving productivity, and can assure existence of paths from fault injected latches to error-observable points in the design.

The method consists of the following steps:


1. Set-up an FV testbench for the design-under-test (DUT). The DUT for error injection analysis typically tends to be functional units, such as the Instruction Fetch Unit (IFU) in a microprocessor design. In general any hierarchy which has error capture artifacts may be analyzed. In its most primitive form the FV testbench consists of setting-up clocks and disabling DFT features such as to put the design in functional mode. In a fully evolved testbench, the interface protocol of the DUT is fully defined as constraints to specify a full "driver" or environment which restricts the execution of the DUT to its legal states. In the latter case FV may be the sole...