Complete and Effective Robustness Checking by Means of Interpolation

Stefan Frehse, Görschwin Fey, Eli Arbel, Karen Yorav, Rolf Drechsler

In: Formal Methods in Computer-Aided Design 2012. Formal Methods in Computer-Aided Design (FMCAD-2012) October 22-25 Cambridge England United Kingdom 2012.


Technology scaling continues to downscale feature sizes. As a side-effect this has some serious drawbacks, in particular increasing vulnerability of circuits against transient faults caused, e.g., by radiation. Even under malfunctions of internal components the circuit must behave as specified. Several techniques have been proposed to overcome this problem. However, the implementation of those techniques in the design might be buggy and needs to be verified. This paper provides an effective algorithm using formal reasoning to completely analyze the fault tolerance of a circuit, under all input sequences and all transient faults. The algorithm based on interpolation identifies components in which transient faults are observable. Experiments show that the newly introduced complete approach analyzes ITC’99 and IBM circuits, effectively.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence