Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core

TL;DR

This paper employs formal verification through model checking to comprehensively evaluate the impact of soft errors on a RISC-V Ibex Core, revealing vulnerabilities and fault effects that are difficult to assess with traditional simulation methods.

Contribution

It introduces a formal verification approach for exhaustive fault analysis in a RISC-V core, providing detailed insights into fault effects and vulnerabilities.

Findings

Misaligned instructions amplify fault effects

Certain bits are more vulnerable to SEUs

Most bits in the core are susceptible to Silent Data Corruption

Abstract

Reliability has been a major concern in embedded systems. Higher transistor density and lower voltage supply increase the vulnerability of embedded systems to soft errors. A Single Event Upset (SEU), which is also called a soft error, can reverse a bit in a sequential element, resulting in a system failure. Simulation-based fault injection has been widely used to evaluate reliability, as suggested by ISO26262. However, it is practically impossible to test all faults for a complex design. Random fault injection is a compromise that reduces accuracy and fault coverage. Formal verification is an alternative approach. In this paper, we use formal verification, in the form of model checking, to evaluate the hardware reliability of a RISC-V Ibex Core in the presence of soft errors. Backward tracing is performed to identify and categorize faults according to their effects (no effect, Silent Data Corruption, crashes, and hangs). By using formal verification, the entire state space and fault list can be exhaustively explored. It is found that misaligned instructions can amplify fault effects. It is also found that some bits are more vulnerable to SEUs than others. In general, most of the bits in the Ibex Core are vulnerable to Silent Data Corruption, and the second pipeline stage is more vulnerable to Silent Data Corruption than the first.