|
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. PeoplePublicationsSoftwareWe 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
SupportThis project receives generous support from the SRC FCRP Gigascale Systems Research Center (GSRC), Microsoft Research, and an equipment grant from Intel. |
