Using formal methods to evaluate hardware reliability in the presence of soft errors

Reliability is a major concern in many embedded systems. Redundancy-based methods are widely used against Single Event Upsets, causing significant temporal and spatial overhead. The traditional method to evaluate the reliability of a system is fault injection. However, it is practically impossible to test all faults for a complex design due to intractable simulation times. In this paper, we propose using formal methods to evaluate hardware reliability in the presence of soft errors. The proposed method can exhaustively search the entire state space and the whole fault list in a reasonable time. The method is applied to assess the vulnerability of all registers in a RISC-V Ibex core.