An Automated Exhaustive Fault Analysis Technique guided by Processor Formal Verification Methods

Endri Kaja1, Nicolas Gerlin1, Bihan Zhao1, Daniela Lopera1, Jad Halabi1, Azam Khan1, Sebastian Prebeck1, Dominik Stoffel2, Wolfgang Kunz2, Wolfgang Ecker1
1Infineon Technologies AG, 2Rheinland-Pfalzische Technische Universit├Ąt Kaiserslautern-Landau


As digital designs become increasingly complex, it is essential to have reliable and automated safety verification techniques. To mitigate the negative impact of faults on design behavior, various hardening techniques are employed. This paper presents a fully automated formal-based fault injection technique for processor designs that can functionally verify safety-critical designs in the presence of faults. The experiments conducted demonstrate that multiple bugs can be detected in different hardening mechanisms without extra effort. Moreover, the proposed technique provides high-confidence fault propagation analysis. The study includes numerous experiments conducted on various processor components of two different RISC-V ISA variants. The experiments achieved better results than simulation-based approaches and at the same time yielded similar results to techniques based on Automated Test Pattern Generation (ATPG) fault propagation analysis.