Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences


UC Berkeley


2008 Research Summary

Verification-Guided Error Resilience

View Current Project Information

Wenchao Li and Sanjit A. Seshia

We propose and demonstrate that algorithmic techniques for formal and semi-formal verification can be gainfully used not just for bug-finding, but also in the construction of error-resilient systems. In particular, we investigate how design verification can be used to estimate a circuit's vulnerability to transient, intermittent, and wearout-related errors, and to reduce the resource overheads of circuit mechanisms for error resilience.

As a first step, we have demonstrated this idea of verification-guided error resilience in the context of soft errors in latches. We show how model checking can be used to identify latches in a circuit that must be protected in order for the circuit to satisfy a formal specification. Experimental results on a Verilog implementation of the ESA SpaceWire communication protocol indicate that the power overhead of soft error protection can be reduced by a factor of five using our approach, for a fairly comprehensive formal specification.

S. A. Seshia, W. Li, and S. Mitra, Verification-Guided Soft Error Resilience, UC Berkeley EECS Department Technical Report No. EECS-2006-118, 2006.