Error-tolerant processors: Formal specification and verification

Ameneh Golnari, Yakir Vizel, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations


There has been significant recent research in reliable architectures. This is in response to the perceived hardware failure threats faced by late- and post-CMOS devices, e.g., energized particle hits, increasing variability of device parameters and aging-related failures. This body of research proposes specific micro-architecture mechanisms to defend against these threats. Each proposed mechanism makes some assumptions about the underlying fault model and addresses some set of errors. Of particular interest are error-tolerant processors which do not guarantee that the processor will execute each instruction strictly as per the ISA, but rather provide a best-effort response to these faults. These processors are suited for application classes which are error-tolerant, e.g. media processing, and thus provide useful output even without strictly implementing their ISA. What is left unsaid is the minimum guarantees that they must provide to result in useful computation. This paper addresses this question. It makes the following contributions (i) It provides a minimum set of properties that such processors must satisfy, e.g., progress and non-accumulating errors, and states these formally using temporal logic for a model of the processor. This model captures not just the error-free function, but also the faults and the error response mechanisms. (ii) We have developed such full-system models for two case studies of recently proposed fault-tolerant processors, YMM [16] and ERSA [5]. (iii) Further, we present the result of model checking these properties for both case-studies and show that they do not fully satisfy these properties.

Original languageEnglish (US)
Title of host publication2015 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages8
ISBN (Electronic)9781467383882
StatePublished - Jan 5 2016
Event34th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015 - Austin, United States
Duration: Nov 2 2015Nov 6 2015

Publication series

Name2015 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015


Other34th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015
Country/TerritoryUnited States

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design


Dive into the research topics of 'Error-tolerant processors: Formal specification and verification'. Together they form a unique fingerprint.

Cite this