With that out in the open, let’s consider the verification of a device involved in the control and safety systems for an autonomous vehicle. A safety or security flaw in any such device may lead to serious consequences. We are talking life or death consequences. Given that, wouldn’t you want the devices that control your autonomous vehicle of the future to be formally verified? The answer should be: Yes!
Fortunately, the good people who brought us the ISO 26262 standard  for automotive safety agree. Like most safety standards, the ISO 26262 standard defines a process by which safety is prioritized through a well-defined hardware development process. Let’s look at some of the steps in that process and how formal verification can play a vital role.
Safety Requirements Traceability
One of the first steps in the process is an analysis phase to determine all the safety related design requirements and their designated level of importance, otherwise called the Automotive Safety Integrity Level (ASIL). The ASIL can be one of four levels, A through D, with D being the highest. The levels are set based on factors such as the related risk of damage or injury, the likelihood of occurrence of a hazardous failure and the control that the user has over the system to minimize the effect of a failure. A requirements management system must be used to provide traceability of the safety requirements through the verification and validation phases to demonstrate that the implemented design meets the requirements. So, something in the test plan must be traceable back to the requirements, whether it be a test, a coverage point or an assertion. Here’s where we find the first application of formal in this process. Assertions that capture safety requirements and are subsequently formally proven will provide the ultimate confidence that the requirements have been met.
Random Failure Analysis
Another key step is the analysis of the effect of random failures on the system. The failures can be transient, such as Single-Event Upsets (SEUs), or permanent due to a component fault. The impact of the failures on safety must be mitigated using mechanisms such as Error Correcting Codes (ECCs) to detect and correct data bit errors and triple modular redundancy (TMR) circuitry. Subsequently, the safety mechanisms must be tested to demonstrate that they are effective in detecting and mitigating the effect of random errors. This negative testing approach involves fault simulation of a potentially enormous number of faults. This is where we find the second application of formal verification in the process. Formal verification tools can be used to pre-qualify the faults before fault simulation to prune out faults that are proven to be redundant or non-propagatable, which reduces the burden on fault simulation.
Avoiding Systematic Failures
The ISO 26262 development process also includes requirements for avoiding “systematic failures”, which is another name for what we commonly refer to as design bugs. The standard recommends that formal verification be used to verify safety related requirements with ASIL level designations of B and above. The standard doesn’t dictate the process, but when they “recommend” something, there better be a good reason to justify going against the recommended approach when it comes time for regulatory review and approval. So, this is where formal property checking can play a huge role in ensuring the safety of these devices and that no latent bugs are going to cause harm or damage. Oski has pioneered the methodology for end-to-end formal sign-off, which ensures that no bugs are left behind after the verification process. This process can be broken down into the four “Cs” of formal sign-off.