Verification-Guided Error Resilience (VGER)

We are investigating the use of formal and semi-formal verification in the construction of systems resilient to device failures including those arising from soft errors, aging, environmental and parameter variations, and aggressive deployment of techniques to reduce resource consumption (e.g., power). Such resilience must be achieved at low overheads on power, performance, area, etc. Defining "resilience" also requires a good specification of system functionality.

A particular focus is the use of formal analysis in the construction of sequential digital circuits resilient to soft errors (both in latches and in combinational logic).

We have also studied techniques for evaluating the quality of specifications, such as vacuity and coverage, in the context of fault-tolerant systems, and techniques to generate specifications from execution/simulation traces.


Daniel Holcomb
Wenchao Li
Sanjit A. Seshia
Orna Kupferman (Hebrew University)
Subhasish Mitra (Stanford)


Scalable Specification Mining for Verification and Diagnosis.
Wenchao Li, Alessandro Forin, and Sanjit A. Seshia.
In Proceedings of the Design Automation Conference (DAC), pp. 755--760, June 2010.

Design as You See FIT: System-Level Soft Error Analysis of Sequential Circuits
Daniel Holcomb, Wenchao Li, and Sanjit A. Seshia.
In Design, Automation and Test in Europe (DATE), pp. 785-790, April 2009.

A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance
Orna Kupferman, Wenchao Li, and Sanjit A. Seshia
In IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), November 2008.

Verification-Guided Soft Error Resilience
Sanjit A. Seshia, Wenchao Li, and Subhasish Mitra.
In Proc. Design Automation and Test in Europe (DATE), April 2007, pages 1442-1447.



We have released BFIT, a tool for estimation of the FIT (failure-in-time) rate of a circuit due to soft errors.

BFIT: The Berkeley FIT Estimation Tool


This project receives generous support from the SRC FCRP Gigascale Systems Research Center (GSRC), Microsoft Research, and an equipment grant from Intel.

  Sanjit A. Seshia, last updated August 2010.