Fault Tolerance and Specification Coverage
Sanjit A. Seshia, Wenchao Li and Orna Kupferman
This project investigates the use of formal techniques to estimate system vulnerability to faults, and thereby significantly reduce the resource overheads (e.g., power) of providing resilience to these faults. We demonstrated the effectiveness of this approach in the context of soft errors in registers. Experimental results on a Verilog implementation of the ESA SpaceWire communication protocol show 4.4X reduction in power overhead for providing soft error resilience.
To achieve certifiable error resilience, we need a good quality formal specification. Our current work addresses this problem from both theoretical and practical standpoints. On the theoretical side, we show that fault tolerance and specification coverage are dual problems. On the practical side, we exploit this duality to iteratively strengthen specifications. We demonstrated our technique with formal verification of a Wormwhole Virtual Channel Router in Verilog. Results indicate that we are able to obtain specifications with tighter latency bounds.
- 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, "On the Duality between Vacuity and Coverage," International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008 (submitted).