How formal concentrates ISO 26262 fault analysis

By Paul Dempsey |  No Comments  |  Posted: March 2, 2017
Topics/Categories: Blog - EDA, - Verification  |  Tags: , , , , ,  | Organizations:

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'.

Fault Pruning

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.

Figure 1. Formal tools trace back the cone of influence for fault pruning of safety goals (Mentor Graphics)

Figure 1. Formal tools trace back the cone of influence for fault pruning of safety goals (Mentor Graphics)

"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.

Figure 2. Anything outside the COI of the detection logic is considered unsafe (Mentor Graphics)

Figure 2. Anything outside the COI of the detection logic is considered unsafe (Mentor Graphics)

"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.

Figure 3. SLEC compares a fault-injected ISO 26262 design with a non-fault-injected copy (Mentor Graphics)

Figure 3. SLEC compares a fault-injected ISO 26262 design with a non-fault-injected copy (Mentor Graphics)

Realizing ISO 26262 fault analysis

In his full paper, Smith discusses the two techniques above in more detail, and in the specific context of their use within the Questa Formal Verification tool from Mentor.

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.

Leave a Comment

PLATINUM SPONSORS

Mentor Graphics GLOBALFOUNDRIES Synopsys Samsung Semiconductor Cadence Design Systems
View All Sponsors