Sanjit A. Seshia and 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},
    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