Verification-Guided Soft Error Resilience
Sanjit A. Seshia, Wenchao Li and Subhasish Mitra
EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2006-118
September 26, 2006
http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-118.pdf
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 five using our approach, for a fairly comprehensive formal specification.
BibTeX citation:
@techreport{Seshia:EECS-2006-118,
Author = {Seshia, Sanjit A. and Li, Wenchao and Mitra, Subhasish},
Title = {Verification-Guided Soft Error Resilience},
Institution = {EECS Department, University of California, Berkeley},
Year = {2006},
Month = {Sep},
URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-118.html},
Number = {UCB/EECS-2006-118},
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 five using our approach, for a fairly comprehensive
formal specification.}
}
EndNote citation:
%0 Report %A Seshia, Sanjit A. %A Li, Wenchao %A Mitra, Subhasish %T Verification-Guided Soft Error Resilience %I EECS Department, University of California, Berkeley %D 2006 %8 September 26 %@ UCB/EECS-2006-118 %U http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-118.html %F Seshia:EECS-2006-118