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.},
}