The safety verification requirements of the ISO 26262 automotive standard are clearly defined but gathering the metrics to show they have been satisfied is more onerous. Formal verification techniques are being promoted as a way of relieving the burden.
Traditional fault simulation can involve the injection of thousands of faults across hundreds of tests - and this number is growing as more is demanded of automotive silicon. Meanwhile, the simulations themselves are far more extensive than necessary - standard simulators cannot distinguish between necessary faults and those that can be ignored.
In a newly published White Paper, Doug Smith, a verification consultant at Mentor Graphics, highlights two techniques which show 'How Formal Reduces Fault Analysis for ISO 26262'. These are 'Fault Pruning' and 'Fault Injection with Sequential Logic Equivalency Checking'.
Formal verification has its foundations in the use of algorithms and heuristics to demonstrate that a design is functionally correct. But from a fault pruning point of view, it has the further capability of being able to trace back from a safety-critical signal to generate a cone of influence (COI) for the logic in a design. So, as ISO 26262 gives clear verification requirements, it provides a starting point from which to do this.
"As part of the ISO 26262 safety analysis, an engineer defines the safety requirements for a design. The first step in fault pruning is removing all design elements not directly in a COI of a safety requirement, and thus [he or she will] consider only the design elements in a COI," Smith writes.
By contrast, those portions outside the COIs can be considered 'safe' and therefore do not require test for the required goals or goals.
However, as Smith notes, this may only be a first step. A data bus may form part of a safety goal or be one in its own right. This is likely to contain error correcting code (ECC), which can be used to reduce the fault injection burden still further. "By pruning that logic whose faults will be detected by ECC, we reduce the number of design elements that need fault injection," Smith continues.
"Likewise the cone of influence can be reduced by applying any top-level constraints (such as disabling DFT, debug and test) or other non-operational modes. As with synthesis, applying these constraints causes the formal tool to reduce the cone of logic, further pruning the faults required to be injected."
Fault Injection with SLEC
Sequential logic equivalence checking is used to compare the outputs from two designs. As a formal technique, it is capable of being used to address both stuck-at and, importantly, transient faults. It can also be used in the observation of single- and multiple-point faults.
"By instantiating a design with a copy of itself, all legal input values are automatically specified for SLEC, just as a golden reference model in simulation predicts all expected outputs for any input stimulus," Smith writes. "The only possible inputs are those values that can legally propagate through the reference design to the corresponding output.
"By comparing a fault-injected design with a copy of itself without faults, the formal tool checks if there is any possible way for the fault to either escape to the outputs or go undetected by the safety mechanism."
This strategy obviates input setup and automates the fault analysis, saving valuable time now that the faults to be injected have been proved. There is no need for a testbench or a test case. Instead, the formal tool needs only definitions for the safety goals as well as the safety detection logic to inject relevant stuck-at and transient faults. And then it reports back.
Realizing ISO 26262 fault analysis
He provides examples of the kind of COI reporting available for pruning and a look at how SLEC differs from better known logic equivalency checking.
The overall benefits that this type of formal approach are numerous. In addition to saving time - even making simulation viable compared with traditional strategies - formal can also deliver a more definitive sense of whether faults are safe or not. It is a powerful weapon given the requirements of ISO 26262.