Error-tolerant processors: Formal specification and verification

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.