Verification-Guided Error Resilience
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.