How to Save a Ton of Time and Energy by Prioritizing Faults with Exhaustive Formal Analysis Before Launching Detailed Fault Verification

By Joe Hupcey III

[Preface: If you are going to be at ARM Techcon 2017 on Wednesday October 25, the methodology described in this article will be part of the presentation “Efficient Register Transfer Level Fault Analysis for Automotive Designs”, given at 11:30am, Mission City Ballroom M3. We will also be at the expo on Wednesday and Thursday in the Mentor booth (606). Join us and ask questions F2F!]

Whether you are tasked with proving your DUT – and the design & verification flow used to create it — meets ISO 26262, DO-254, IEC 60601, IEC 61508, Mil-Std 882, or any one of a host safety standards, you will have to:

A) Map out where any faults could occur in the DUT

B) Determine which of these faults would cause something really bad to happen, and which would be a mere inconvenience

Let’s presume that (A) has been completed – and the resulting list of fault points seems overwhelming. What can be done to make step (B) manageable, and effectively determine the subset of faults in a given design that will affect a safety requirement?

First, the initial leap from (A) to (B) is the realization that not all faults will result in disaster. In logic design terms, any design elements that are not in the logic fan-in of a safety critical output signal are essentially safe. Thus, the key to “fault pruning” is to determine which faults are inside or outside the safe logic areas.

Fortunately, this type of analysis is a strength of formal property checking. Specifically, formal tools have the ability to exhaustively trace back from an output to show all the upstream logic that affects the output signal. This is called the “cone of influence”, and in the context of a fault pruning process it means that any design elements not in the cone of influence of a safety-critical output signal are considered safe and do not need to be tested.

Figure 1: Formal tools trace back the cone of influence to perform their analysis.

Putting this into a more concrete example, in the figure below the cones of influence for the data output (data_o) and the output from an error correcting code circuit (ecc_error_o) are concurrently analyzed by the formal tool. Rephrasing, the formal tool traces through the logic of the design, finding all the major elements in the cone of influence back to the primary input ports. (Formal tools can also give finer grain details, such as information about the signals or nets between the state elements; and can also prove which states are unreachable.)

Figure 2: Anything outside the COI of the detection logic is considered unsafe

The next step is to look at what design elements in the cone of influence of a safety requirement overlap with the cone of the safety detection mechanism. For example, suppose a data bus is considered safety critical. Along with the data bus are extra error-correcting code (ECC) bits for detecting any errors. As long as the ECC bits flag any transient faults, the data bus is considered safe because it can be detected and dealt with downstream. Any design elements in the cone of logic of the data bus that are not in the cone of the ECC logic cannot be detected by the safety mechanism and so must be considered unsafe.

Taking a step back to the overall project view: we recommend this formal fault pruning should be done as early as possible in the design cycle so that various optimizations and tradeoffs can be made. Once the design is stable, the next step is to start injecting these critical faults into the ongoing verification flow. In a future post (and in the ARM Techcon presentation), we will show how the next step is to take the golden “no fault” model and a fault injected model into a formal-based sequential logic equivalence checking (SLEC) flow to analyze the results and to determine the effectiveness of the safety mechanisms.

Until then, may your coverage be high and your power consumption be low,

Joe Hupcey III, Ping Yeung, Doug Smith

Reference links:

Related ARM Techcon 2017 presentations in Mentor’s booth theater (booth 606): Wednesday, 10/25, 10:30am and Thursday, 10/26, 11:30am: “Innovations in Automotive: Driving Functional Safety Verification” tech talk

Whitepaper: How Formal Reduces Fault Analysis for ISO 26262
https://www.mentor.com/products/fv/resources/overview/how-formal-reduces-fault-analysis-for-iso-26262-82758134-85e7-4753-92f4-6f90e36e7d96

The aforementioned presentation’s listing in the ARM Techcon 2017 program guide:
Efficient Register Transfer Level Fault Analysis for Automotive Designs
http://schedule.armtechcon.com/session/efficient-register-transfer-level-fault-analysis-for-automotive-designs/853217