Endri Kaja

• The semiconductor industry is experiencing rapid growth, which is driving the need for innovative development methodologies, particularly in the digital design domain. In addition to ensuring correct behavior, designers must guarantee that the chips operate at predefined levels of reliability when used in automotive products. Safety considerations have become an integral part of the development process following the adoption of the ISO 26262 safety standard for automotive safety-critical systems. ISO 26262 ensures that these systems behave according to required safety levels by mitigating the risk of hazardous malfunctions. The standard recommends fault injection to verify and analyze safety-critical systems; however, this process often proves to be laborious and error-prone. To combat these challenges, advanced and automated methods are required. Accordingly, this thesis automates the safety verification process, utilizing model-driven architecture principles to enhance productivity, quality, and reliability. The thesis proposes the generation of mixed-granularity models to represent designs, where gate-level models represent safety-critical components and Register-Transfer Level (RTL) represents the rest of the design. The mixed-granularity model is achieved through model transformation, and formal equivalence checks are applied during this process to ensure the correctness of the transformation. This approach also enables fault injection directly into the design, reducing the overhead caused by the use of additional fault injection tools. The absence of bugs of this process is guaranteed by equivalence check. Furthermore, the ability to inject faults at the design level has enabled the development of a novel fault emulation framework utilizing FPGAs. This proposed framework scales well to large hardware designs and has been successfully applied to several RISC-V based CPU subsystems with a runtime advantage over traditional simulation-based fault injection frameworks. Moreover, an automated flow based on formal methods has been developed that verifies the functionality of design hardening mechanisms and their integration into processor designs. This flow delivers high-quality verification results without requiring white-box design knowledge. Furthermore, the thesis introduces an automated and efficient approach for generating Software-Based Self Tests (SBST) tailored for RISC-V processor cores. This method involves testing processor cores through instructions, providing a viable alternative to hardware-centric solutions. Additionally, the SBST is combined with a novel Program Flow Checking (PFC) technique to achieve high fault coverage and high fault detection rates that comply with ISO 26262 requirements. The proposed PFC is a mixed hardware/software solution that detects faults by monitoring program flow execution. The proposed solutions have proven to be effective in numerous industrial designs. The achieved results demonstrate that automated approaches significantly reduce development costs and are less susceptible to errors. Through a holistic generation flow, multiple safety verification techniques have been explored, encompassing methods based on simulation, emulation, and formal verification.