Generator-Driven Functional Safety for RISC-V SoCs with Formal Assurance
2026-06-10 , Poster Island D

Functional safety (FuSa) in modern SoC designs demands rigorous fault detection mechanisms alongside standardized error reporting. We present a fully automated, generator-driven design flow that automatically applies dual modular redundancy (DMR) through a pass implemented in CIRCT, an MLIR-based hardware compiler framework, without requiring manual RTL modification. To validate the correctness of the generated design, we apply formal verification, providing strong assurance that the DMR composition itself introduces no spurious faults. In addition, we address the system-level integration of the generated fault detection signals by routing them to a safety controller that adheres to the "RISC-V RERI Architecture Specification" for error reporting across the SoC, capturing each error's severity, nature, and location. We validate our generation flow through fault injection, demonstrating reliable fault detection across arbitrary hardware modules and correct propagation, recording, and reporting of detected errors in the safety controller. Combined, our contributions form an automated path from module-level fault hardening to system-level error observability, advancing the practical adoption of FuSa practices in generator-based RISC-V SoCs.

Frederik Haxel is a researcher at the FZI Research Center for Information Technology. His research interests include developing tools and methods to accelerate the design of safe and efficient RISC-V systems.