Verification-Guided Soft Error Resilience
Sanjit A. Seshia, Wenchao Li, and Subhasish Mitra. Verification-Guided Soft Error Resilience. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE), pp. 1442–1447, ACM Press, April 2007.
Download
Abstract
Algorithmic techniques for formal verification can be usednot just for bug-finding, but also to estimate vulnerabilityto reliability problems and to reduce overheads of circuitmechanisms for error resilience. We demonstrate this ideaof verification-guided error resilience in the context of softerrors in latches. We show how model checking can beused to identify latches in a circuit that must be protectedin order that the circuit satisfies a formal specification. Experimentalresults on a Verilog implementation of the ESASpaceWire communication protocol indicate that the poweroverhead of soft error protection can be reduced by a factorof 4.35 by using our approach rather than protecting alllatches.
BibTeX
@inproceedings{seshia-date07, author = {Sanjit A. Seshia and Wenchao Li and Subhasish Mitra}, title = {Verification-Guided Soft Error Resilience}, booktitle = {Proceedings of the Conference on Design, Automation and Test in Europe (DATE)}, pages = "1442--1447", month = "April", publisher = {ACM Press} year = {2007}, abstract = {Algorithmic techniques for formal verification can be used not just for bug-finding, but also to estimate vulnerability to reliability problems and to reduce overheads of circuit mechanisms for error resilience. We demonstrate 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 that the circuit satisfies 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 4.35 by using our approach rather than protecting all latches.}, }