GOF Formal

GOF Formal is one of the function components integrated in GOF platform. It provides a formal method to calculate fault coverage in an IC design in functional safety.


ISO26262 defines functional safety as "the absence of unreasonable risk due to hazards caused by malfunctioning behavior of electrical and electronic systems". Four ASILs are proposed to represent four degrees of automotive hazards. In IC component, the coverage in the ASIL requirement is the fault coverage in the logic circuit. Specifically, single point fault metric (SPFM) and latent fault metric (LFM) should meet minimum numbers for the corresponding ASIL levels. The following table lists the three ASIL levels with specific coverage numbers defined in the standard.


The traditional method to calculate the fault coverage is pure simulation based. It's inefficient and time consuming. GOF Formal provides a formal and efficient way to calculate the SPFM and LFM numbers of a logic design. It can work in a standalone mode to calculate the coverage metric. And it can also work as a supplemental method to cover the faults left over from simulation based process.

Single Point Fault and Latent Fault

Single point fault (SPF) is the fault in the IC design that leads directly to the violation of a safety goal which is defined as observation point in the "Cone of Influence" section below and no fault in the IC circuit is covered by any safety mechanism. However, if there is safety mechanism, but the fault can't be covered by the safety mechanism, the fault is called residual fault according to the standard. In calculating SPFM, residual fault is treated as single point fault. Latent faults are multiple-point faults not detected by a safety mechanism or perceived by the driver. The latent fault metric is to determine whether coverage by safety mechanisms is sufficient to protect against risk from latent faults in the IC design.

Fault Model

GOF Formal injects faults to each input port and each pin of logic gates. Each input port has stuck-at 0 and stuck-at 1 faults injected. Every combinational gate has stuck-at 0 and stuck-at 1 faults injected into each pin. For flip-flop, stuck-at 0 and stuck-at 1 faults are injected into each data and clock pin. And flip-flop has Single Event Upset (SEU) fault injected to the state in random time.

Figure 1: Fault model for logic gates

Cone of Influence

SPFM and LFM metrics can be calculated in two methods, rough mode and detail mode. The rough mode is done by structural analysis of the Cone of Influence. The detail mode is calculated by formal analysis of the Cone of Influence.

Two types of strobing points shall be defined for the Cone of Influence extraction.

The observation points are the outputs or registers that are impacted by the injected faults which affect functional safety and violate safety goal. The diagnostic points are the outputs or registers to check if injected faults can be detected at these strobing points or perceived by the up level driver.

The logic back traced starting from the observation points and the diagnostic points all the way to the inputs or black boxes. The Cone of Influence (COI) is created for the observation points and the diagnostic points respectively. Each cell and each input port in the cones will be injected faults according to the Fault Model section.

Figure 2: Cone of Influence

SPFM and LFM calculation

The rough mode merit calculation can be run by using COI structural analysis.

In the figure 2, all faults that are outside of the two COIs are safe faults.

Area A has faults that are observable but not detectable, so they can be classified as residual faults. And they can be classified as single point faults if safety mechanism is not implemented for the design, in which case the diagnostic points are not present and Area B and Area C are zero size.

Area B has faults that are classified as multiple point faults since they are observable and detectable by the structural analysis.

Area C has faults that are classified as detectable multiple point faults, but they are not observable. Formal verification will be run on Area B and Area C to check if the faults in the two areas can not propagate to the diagnostic points, then they can be classified officially as latent faults.

The Single Point Fault Metric (SPFM) can be calculated according to the following equation.

SPFM = 1 - Σ(λSPF+λRF)/Σ(λ)


λSPF: Single Point Fault when there is no safety mechanism

λRF: Residual Fault

λ: Any Fault

The Latent Fault Metric (LFM) can be calculated according to the following equation.

LFM = 1 - Σ(λMPF_UD)/Σ(λMPF - λSPF - λRF)


λMPF_UD: Multiple Point Fault not detected by the driver

λMPF: Any Multiple Point Fault

λSPF: Single Point Fault when there is no safety mechanism

λRF: Residual Fault

In the rough method calculation, Σ(λSPF+λRF) are the faults in Area A. Σ(λMPF_UD) are the unobservable and undetectable faults. LFM is 100% in the rough analysis method, since there is no unobservable and undetectable fault from the point of view of COI structure.

Faults Injection Formal Verification

Formal analysis needs to be run to fine tune the final accurate metrics. For each fault injected, GOF Formal either proves that a path exists to propagate the fault to the observation or diagnostic points, or disprove there is such path. A path means by toggling input ports in some limited clock cycles, the fault can propagate to the observation/diagnostic points.

GOF Formal doesn't require stimulus nor is a testbench required. The tool automatically determines the stimulus. For each fault injected, two designs are compared to see if the specified outputs are equal. One design is the fault injected design, the other is the original design. The specified outputs are the observation points or the diagnostic points set by user. The faults to be injects can be thousands or millions. GOF Formal uses cluster command to fully utilize the cluster computing power. Thousands of jobs can be submitted in parallel to the cluster machines with only one license being used.

Metrics Improvement

In order to improve the fault coverage, safety mechanisms should be built in the IC design. There are several approaches for safety mechanism implementation.

In the figure 2, a safety mechanism can be a double modular design or ECC design. The diagnostic points would be the alarm bits in the double modular error bit, or ECC error recovering signals. For SPFM metric improvement, those gates in Area A that are not covered by safety mechanism can be modified to support TMR (Triple Module Redundancy), so that λSPF can be further reduced and SPFM improved accordingly. See this TMR ECO Case


Please see GOF Formal Use Cases for more information.

For other usages and flows, check Online Manual for more detail

Follow us:
NanDigits.com US | NanDigits.cn China
© 2022 NanDigits Design Automation. All rights reserved.