Formal Safety Verification of Automotive Microcontroller Parts

Abstract:
Automotive microcontrollers have to meet the ISO 26262 functional safety standard for road vehicles in order to be certifiable for applications in safety-critical systems according to defined automotive safety integrity levels. An automotive microcontroller system therefore includes various safety mechanisms implemented in hardware and software which provide robustness against defects during a driving cycle and monitor failure modes of functional parts. These extra measures increase the design complexity significantly and entail additional verification effort for proving that the safety requirements are met. The quantity and variety of potential faults to be considered poses a huge verification problem hardly solvable by simulation alone. This paper presents a formal verification methodology for 100% fault coverage of register safeguarding measures at register-transfer level in vital parts of automotive microcontroller chip products.