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

Abstract

This study employs formal verification, specifically model checking, to exhaustively evaluate the hardware reliability of the RISC-V Ibex Core against Single Event Upsets (SEUs), overcoming the coverage limitations of simulation-based fault injection. Utilizing backward tracing, the researchers categorized faults as Silent Data Corruption (SDC), crashes, or hangs by exploring the entire state space and fault list. Key findings indicate that misaligned instructions amplify fault effects and that the second pipeline stage is significantly more vulnerable to SDC compared to the first stage.

Report

Key Highlights

• Novel Methodology: Formal verification (model checking) is used for exhaustive reliability evaluation, replacing traditional, coverage-limited simulation-based fault injection.
• Target System: The analysis focuses on evaluating hardware reliability in the presence of soft errors (SEUs) within a specific RISC-V processor, the Ibex Core.
• Exhaustive Coverage: The approach ensures the entire state space and fault list are explored, providing high-accuracy fault coverage not feasible with random fault injection.
• Key Vulnerability: Misaligned instructions are found to significantly amplify the effects of injected faults.

Technical Details

• Error Type: Single Event Upsets (SEUs), or soft errors, defined as the reversal of a bit in a sequential element.
• Verification Technique: Formal verification in the form of model checking.
• Fault Identification Method: Backward tracing is performed to classify the consequences of SEUs.
• Fault Categories: Fault effects are categorized into four types: no effect, Silent Data Corruption (SDC), crashes, and hangs.
• Architectural Findings:
  • Most bits in the Ibex Core are vulnerable to SDC.
  • The second pipeline stage is reported to be more vulnerable to SDC than the first pipeline stage.

Implications

• Improved Reliability Standards: This work validates formal verification as a superior, high-integrity alternative to standard simulation methods (often suggested by standards like ISO26262) for assessing soft error vulnerability in complex chip designs.
• Enhanced RISC-V Robustness: The specific identification of vulnerabilities within the open-source Ibex Core (such as the second pipeline stage and instruction handling) provides critical data for hardware developers seeking to harden RISC-V cores for safety-critical and high-reliability embedded systems.
• Design Guidance: The findings offer specific guidance for future hardware design choices, suggesting designers prioritize hardening mechanisms around registers or logic associated with misaligned instruction handling and the later stages of the processor pipeline to mitigate SDC.