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

TL;DR

This paper tackles the reliability challenge posed by SEUs in embedded hardware by proposing a formal verification framework that uses backward fault tracing and model checking to exhaustively identify SEUs in a RISC-V Ibex Core. The approach defines formal properties (SDC, crash, and hang) and employs both strobe and architectural strategies with SystemVerilog Assertions to locate vulnerable bits without resorting to exhaustive fault injection. Key contributions include a four-step method for SEU identification, an RTL fault-injection mechanism implemented with XOR gates, memory abstraction to control state-space growth, and comprehensive results showing which bits are most susceptible, with misaligned instructions amplifying fault effects and the second pipeline stage being particularly vulnerable to SDCs. The work demonstrates how formal verification can provide exhaustive SEU analysis, enabling targeted, cost-efficient protection strategies and guiding robust hardware design in safety-critical applications. Future extensions aim to address Double Event Upsets and further mitigate state-space explosion while maintaining exhaustive search capabilities.

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.

Figures (2)

• Figure 1: Ibex Pipeline from ibex
• Figure 2: (a) Forward tracing of faults using fault injection (b) Backward tracing in this work