Where formal verification can help in functional safety analysis

Formal techniques seem to be a way to cope with the exploding complexity of functional safety analysis. Here, the overall fault propagation probability to a certain safety-point in the design must be analyzed. As a consequence, the careful verification of the design is no longer sufficient. In addition, the propagation of all possible faults potentially showing up at all of the design's internal nodes must be validated. But this is not only a complexity challenge. Safety standards have a probabilistic view on functional safety analysis results and aspects such as different fault and pattern probability must be considered and related to requirements such as confidence level and maximum FIT rate. Following an overview on verification challenges around functional safety analysis, we introduce our innovative concept on how formal formal techniques can substantially simplify industrial functional safety analysis flows. Given a transient fault, the conditional error propagation probability must be analyzed. An error has propagated if it did eventually cause a counterexample to a safety property. If we can prove formally that such a counterexample is not possible, we have shown that the fault was not critical. We have to estimate how often on average faults will propagate. For this purpose a test bench traditionally generates input pattern sequences and then Monte Carlo fault injection is performed. Simulations are continued for evaluating the effects of the injected faults. In this paper we show how invariants generated with property directed reachability (PDR) model checking can be used to speed up traditional Monte Carlo fault injection. The invariant obtained with PDR can be used to show that the system remains safe after injected faults. Unnecessary simulations are avoided and a significant speedup for sample evaluation is obtained.