Verification-Guided Error Resilience (VGER)
Daniel Holcomb, Wenchao Li and Sanjit A. Seshia
Gigascale Systems Research Center
This project investigates the use of formal and semi-formal verification techniques to achieve resilience to device faults at low resource (e.g., power) overhead. A verification-guided approach is used to estimate system vulnerability to device faults and pin-point circuit components that contribute significantly to the system-level failure rate. The effectiveness of this approach is demonstrated for soft errors.
In earlier work, we focused on soft errors in latches. Formal verification was used to identify latches that do not affect system correctness and thus can be left unprotected. Experimental results on a Verilog implementation of the ESA SpaceWire communication protocol show 4.4X reduction in power overhead for providing soft error resilience.
In more recent work, we deal with soft errors both in sequential and combinational elements. The verification-guided methodology computes system-level failure in time (FIT) rate by using a judicious mix of gate-level simulation and system-level failure analysis. Our gate-level simulation technique is efficient and accurate, incorporating effects of logical, timing, and electrical masking. System-level failure is detected by monitors synthesized from formal specifications. Failure rate is computed by statistical estimation from sequential simulations with random soft error injection. Experimental results show that our methodology is efficient, and provides useful information for designers to perform Pareto-optimal hardening to synthesize reliable and low overhead circuits.
- S. A. Seshia, W. Li, and S. Mitra, "Verification-Guided Error Resilience." Proc. Design Automation and Test in Europe (DATE), April 2007, pp. 1442-1447.
- O. Kupferman, W. Li, and S. A. Seshia, "A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance," Proc. 2008 Formal Methods in Computer Aided Design Conf., IEEE Press, 2008.