Four Steps To ISO 26262 Safety Mechanism Insertion And Validation

An automated workflow using safety synthesis and formal verification can help address random faults with safety mechanisms.

popularity

By Ping Yeung, Jin Hou, Vinayak Desai, and Jacob Wiltgen

The complexity of automotive integrated circuits (ICs) has grown exponentially with the introduction of advanced driver-assistance systems and autonomous-drive technologies. Directly correlated to this hike in complexity is the increased burden of ensuring an IC is protected from random hardware faults—functional failures that occur unpredictably.

Historically, the automotive industry has addressed safety analysis by leveraging expert judgment. The initial safety analysis has been commonly performed top-down using Failure Modes Effects Diagnostic Analysis (FMEDA). With the increase in IC complexity, a primarily expert-driven approach is no longer practical or effective.

Automotive ICs have become too large and complex to expect a human to fully comprehend the safety mechanisms required to protect all the possible failures. An automated workflow must be deployed to assist experts in addressing random faults. An efficient approach is to use safety synthesis and formal verification to incorporate safety mechanisms into the design. This is best to be done at the register transfer level (RTL), where functional verification can be performed efficiently. The process can consist of these major steps:

  • Safety Exploration: Explore areas of the design where better fault detections are required
  • Safety Mechanism Insertion: Use safety synthesis to introduce safety mechanisms that have the right tradeoff for the RTL structures
  • Design Change Validation: Validate the design changes with formal verification
  • Formal Fault Injection: Perform formal fault injection to measure the diagnostic coverage

Safety exploration

The goal of safety exploration is to identify optimal safety architecture and safety mechanisms. Safety mechanisms come in a variety of flavors, each with its own level of effectiveness in detecting random hardware faults. During safety exploration, a series of “what-if” scenarios are performed to understand the impact of different safety mechanisms on the design, especially with respect to power, area, performance, safety metrics, and diagnostic coverage. We recommend this exploration be done without modifying the design so that simultaneous analyses can be performed quickly and efficiently. If this is performed early in the design process, safety exploration will help design teams meeting the safety targets successfully after insertion and verification.

Safety mechanism insertion

Modifying a legacy design to introduce safety mechanisms can be an error-prone process. The situation becomes worse if the initial safe mechanism does not meet the safety goal, and a different mechanism has to be used. Hence, safety synthesis is a new approach to augment design structures to improve fault tolerance. To create a safety architecture for legacy designs, safety synthesis introduces two types of safety mechanism automatically. One is used at the register-level, and the other is used at the module level.

For each safety mechanism, there are tradeoffs concerning efficiency, fault detection latency, and area overhead. Figure 1 shows where safety mechanisms can be used in a safety-critical design.

Figure 1. Example Safety Mechanisms for a Safety-Critical Design

For the design interfaces, parity checks can be performed to ensure accurate data transmission between the interface modules and the interface controllers inside the design. Once the data are inside the design, they can be protected with data parity on the buses and error-correction code (ECC) in the storage elements. On-chip bus transactions can be observed by dedicated bus monitors. Critical control components, such as functional safety mechanisms and arbitration logic, will best be protected with triple module redundancy and majority voting. Central and embedded processors can be protected with double modular redundancy along with lockstep checkers.

Register-level insertion is more surgical. It inserts safety mechanisms in the storage elements, such as register duplication and parity. This approach is commonly used to protect control and state machine structures. Some register- level safety mechanisms include:

  1. Parity generation and checking for critical control elements
  2. Double modular redundancy for a selected list of registers
  3. Triple modular redundancy for a selected list of registers
  4. Error correction, and single-error correction with double-error detection for banks of registers
  5. Protocol checking ensures valid state transitions for finite state machines

Safety synthesis can add parity checking to all or a list of special registers in a module.

Figure 2. Parity generation and checking for control registers

ECC can also be used for a bank of registers. In this mode, safety synthesis groups the registers by name and adds ECC by creating a syndrome. Later, the syndrome is used to determine whether there is an error and to recover the error from it. For finite state machines, safety synthesis will elaborate the valid state space and the state transition matrix to build a protocol checking safety mechanism.

Module-level insertion creates redundancy-based safety mechanisms at the instance level. Some module-level safety mechanisms include:

  1. Double modular redundancy along with lockstep checker
  2. Triple modular redundancy along with lockstep checker and majority voting
  3. Input and output parity checking on groups of interface signals
  4. Memory parity generation and checking

As shown in Figure 3, safety synthesis creates a second instance of the module and makes appropriate connections for all the outputs and inputs between the first and second instance, along with the lockstep checker.

Figure 3. Double modular redundancy along with lockstep checker.

Design change validation

Sequential Logic Equivalence Checking (SLEC) formally verifies that two designs are functionally equivalent using formal verification technology, Figure 4. The implementation of the two designs can be different as long as the out- puts are always the same. When SLEC proves the equivalence of two signals, one from each design, the two signals are equivalent for all inputs and for all times. If any signal pair are not equivalent, SLEC automatically generates an error trace using waveforms to show the cause-and-effect of the problem. When all outputs of the two designs are proven equivalent, we can be confident that the two designs are functionally equivalent.

Figure 4. Sequential Logic Equivalence Checking

Hence, SLEC can be used to verify:

  • Safety Mechanism Insertion: ensures that the functionality of the original design is not changed by the addition of the safety mechanisms
  • Safety Mechanism Operation: ensures that the inserted functional safety mechanisms are working as

After the insertion of safety mechanisms, it is essential to ensure that the designs before and after insertion are functionally equivalent. Instead of verifying the functionality of the safety mechanism instrumented design using simulation regression, SLEC is a more direct and comprehensive approach.

In Figure 5, triple modular redundancy (TMR) is used as the safety mechanism to protect the design. By comparing Design A (without safety mechanism) and Design B (with TMR), SLEC can mathematically prove that the TMR has been correctly inserted into the design. This approach gives us better confidence as functional simulation can only simulate limited numbers of input sequences to verify the operation of the TMR.

Figure 5. Safety Mechanism Insertion Verification with SLEC

Formal fault injection

Now we need to make sure the safety mechanism is working correctly to protect the design from possible failures. After the safety mechanisms have been introduced, fault injection can be performed with a formal-based methodology. Failure mode and effects analysis can determine whether the safety mechanism is sufficient. The formal methodology is set up to inject both stuck-at and transient faults into a design, clock the fault through the design’s state space, and see if the fault is propagated, masked, or detected by the safety mechanisms.

As depicted in Figure 6, a golden (no-fault) model and a fault injected model are used to perform on-the-fly fault injection and result analysis. 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. By comparing a fault injected design with a copy of itself without faults, the formal tool checks if there is any possible way for a fault to either escape to the outputs or go undetected by the safety mechanism.

Figure 6. Safety Mechanism Operation Verification with Formal-based Fault Injection

For more on this topic and results of using this approach on real designs, please download the whitepaper Are You Safe Yet? Safety Mechanism Insertion and Validation.

Ping Yeung, Ph.D. is the Principal Engineer in the functional verification division of Mentor, A Siemens Business. He has over 20 years application, marketing, and product development experience in the EDA industry, including positions at 0-In, Synopsys, and Mentor Graphics. He holds 9 patents in the CDC and formal verification areas.

Jin Hou, Ph.D. is a product engineer for Questa Formal at Mentor, A Siemens Business, with more than 12 years in formal and assertion-based verification. Hou has worked as both a CAE and PE, with experience in product definition, customer support, tool testing, customer training, technical marketing, and, currently, as a PE for the Questa Formal Apps. Hou earned her Ph.D. at Université de Montréal, Montreal, Canada.

Vinayak Desai is a solutions engineer for Functional Safety products at Mentor, A Siemens Business. With over 18 years in the EDA and semiconductor industries, Desai has worked as both a CAD engineer and as an FAE supporting static tools for DFT, CDC, lint, power, synthesis, and implementation tools. He is currently focused on functional safety solutions, product definitions, customer evaluations, tool testing, AE training, and technical marketing. Desai earned an M.S. at California State University, Northridge.

Jacob Wiltgen is the Functional Safety Solutions Manager for Mentor, A Siemens Business, and is responsible for defining and aligning functional safety technologies across the portfolio of IC Verification Solutions .  Prior to Mentor, Wiltgen has held various design, verification, and leadership roles performing IC and SOC development at Xilinx, Micron, and Broadcom. He holds a Bachelor of Science degree in Electrical and Computer Engineering from the University of Colorado Boulder. 



Leave a Reply


(Note: This name will be displayed publicly)