Error-tolerant processors: Formal specification and verification

Ameneh Golnari, Yakir Vizel, Sharad Malik

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

5 Scopus citations

Abstract

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.
Pages286-293
Number of pages8
ISBN (Electronic)9781467383882
DOIs
StatePublished - Jan 5 2016
Event34th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015 - Austin, United States
Duration: Nov 2 2015Nov 6 2015

Other

Other34th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015
CountryUnited States
CityAustin
Period11/2/1511/6/15

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design

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

  • Cite this

    Golnari, A., Vizel, Y., & Malik, S. (2016). Error-tolerant processors: Formal specification and verification. In 2015 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015 (pp. 286-293). [7372582] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICCAD.2015.7372582