Efficient handling of the fault space in functional safety analysis utilizing formal methods

Circuit robustness can be increased with selective Flip-Flop hardening. Finding candidate sets of Flip-Flops for optimal selective hardening requires costly fault simulations, in particular if we consider safety properties stating that a bad state should never be reached in future. We present a fully symbolic formal method that gives a rigorous robustness measure without the need of extensive fault simulation and that can be applied in early design stages for selective hardening. Using Formal Verification, we define, compute and measure a set of “critical transitions”. The Markov Property is not required for the proposed method.