How Formal Reduces Fault Analysis for ISO 26262

The ISO 26262 standard defines straightforward metrics for evaluating the “safeness” of a design by defining safety goals, safety mechanisms, and fault metrics. However, determining those metrics is difficult. Unlike simulation where it is never known if the design has been simulated enough or given enough input, formal verification conclusively determines if faults are safe or not, making the failure rates from formal analysis more than an arbitrary number determined by fault simulation.

Formal analysis tools that apply SLEC techniques are an ideal solution for fault pruning, fault analysis, and determining diagnostic coverage. This paper discusses how to use formal verification for static and transient fault analysis to generate ISO 26262 safety metrics, first describing fault pruning and then the more sophisticated fault injection using SLEC.

Limitations of Fault Simulation

The ISO 26262 standard defines straightforward metrics for evaluating the “safeness” of a design by defining safety goals, safety mechanisms and fault metrics. However, determining those metrics is difficult. Systematic failure analysis can find simple faults, such as stuck-ats, but random hardware failure analysis, which poses a much harder challenge, is usually tackled through a process of fault analysis, including fault injection. Traditionally, safety analysis is handled by a fault simulator. Fault simulators use existing tests and regressions and randomly inject faults during simulation to determine if the injected fault impacts safety critical outputs.

There are many possible methods. For example, using a simulation waveform dump from a golden run, a fault simulator injects faults and compares the results against the expected waveform to see if the fault eventually becomes masked or violates a safety requirement (e.g., a safety critical signal). Verification engineers use this fault information to calculate failure rate metrics (defined in the ISO 26262 standard) or diagnostic coverage, which is the proportion of the failure rate detectable or controlled by a safety mechanism. Or they use it to conduct function injection tests, which determine the effectiveness, correctness and timing of a safety mechanism.

A complete safety analysis requires that engineers inject thousands of faults into hundreds of tests and simulate them to their outputs. This exponentially exploding workload swamps a simulation-based fault grading system. Additionally, simulators cannot determine which faults can be safely ignored, so they simulate a much larger list of faults than necessary. These issues force simulation-based fault testing systems to test a statistically insignificant number of safety-critical faults.

Advantages of Formal Verification

A better approach and alternative to using fault simulation is using a formal verification technique known as property checking or model checking. Formal verification avoids the slowness of event-simulation by using mathematical algorithms and heuristics to prove the functional correctness of a design. Formal verification systems can also trace back a cone of influence from a safety critical signal or expression in order to prune the
code of logic and reduce analysis time. However, where formal really excels is in determining transient faults.

Transient faults, such as a single event upset (SEU), occur while a design is operating. Formal engines have the ability to inject faults and formally prove whether the faults affect a safety requirement. Achieving a proof in simulation is usually impossible since it requires testing every possible input combination, but with formal technology, the safeness of a safety requirement can often be known absolutely and with the entire safety requirement’s state space covered.

Consequently, formal tools explore both legal and illegal state spaces. This is easily remedied, however, using a technique called sequential logic equivalency checking (SLEC), which allows engineers to avoid testing invalid or undefined input paths. Using SLEC, the inputs do not need to be constrained (except as needed for clocks, resets and any tied-mode bits), making formal verification an ideal method for performing safety analysis.