Using formal verification for designing hardware designs free from logic design bugs has been an active area of research since the last 15 years. Technology has matured and we have a choice of formal tools such as model checkers, equivalence checkers, and a range of theorem provers. Hardware reliability and fault tolerance has been studied for a long time as well, and some good solutions in the form of redundancy are available for making hardware resilient against faults. However, understanding the impact of a particular kind of fault known as a single-event-upset (SEU) or a transient fault especially in the context of low-power design is not well understood, and therefore achieving adequate tolerance for low-power processors against SEUs is still very much an open problem. A significant bottleneck in this has been the traditional fault injection methodology whereby the impact of a fault is analysed whilst a processor is running a specific binary program image. Thus the true impact of...
Ashish Darbari, Bashir M. Al-Hashimi