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://www2.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://www2.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://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-118.html
%F Seshia:EECS-2006-118