Tags:Automotive Microcontroller Design, Formal Verification, Integration Verification, ISO 26262, Register Hardening with Library Components, Safety Design Automation and Structural Design Analyses
Abstract:
Abstract- According to the automotive ISO-26262 standard, random bit-errors in registers controlling safety-critical function in modules of microcontroller SoCs for vital applications need to be detected to allow the system to prevent dangerous failure modes by taking adequate and timely reactions to drive the system into a safe state before potential harm is caused to human lives. Using a library of formally pre-verified parametric safety components, a specific register monitoring mechanism has so far been manually integrated in many modules of automotive microcontroller product families. The integration of these library components must follow certain well-defined rules, which is then ensured by dedicated integration checks of the modules. We have taken the next step: Having demonstrated that the integration verification of this safety mechanism can be automated, we felt that the previously manual integration process itself should also be automatable. This paper summarizes how automatic analysis and verification routines are enhanced to fully automate the installation of the safety mechanism in such a way that not only substantial manual design effort is saved, but also correctness by construction is achieved.
Automatic Insertion of a Safety Mechanism for Registers in RTL-Modules