NDLI: Error-tolerant processors: Formal specification and verification

Content Provider	IEEE Xplore Digital Library
Author	Golnari, A. Vizel, Y. Malik, S.
Copyright Year	2015
Description	Author affiliation: Dept. of Electr. Eng., Princeton Univ., Princeton, NJ, USA (Golnari, A.; Vizel, Y.; Malik, S.)
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.
Starting Page	286
Ending Page	293
File Size	1644629
Page Count	8
File Format	PDF
e-ISBN	9781467383882
DOI	10.1109/ICCAD.2015.7372582
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2015-11-02
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Program processors Hardware Transient analysis Computer architecture Reliability Computer crashes
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in