With the increasing availability of computational resources and the progress in research concerning automated formal methods, the characterization of safety features for hardware requires improved precision in functional vulnerability detection. In the context of formal fault injection, the model checking algorithm can be used to detect vulnerabilities in digital systems by violating the nominal temporal properties. We present a general methodology to reduce the state space that is computed and traversed during these fault campaigns. The chosen criteria preserves the nominal behavior and the failure modes, expressed by the fault-violated properties. This process is crucial to provide a manipulable object for subsequent Failure Mode and Effects Analysis. Finally, we propose an assumption-based guarantee technique to model how a fault may propagate through different hardware units, for a scalable methodology of formal fault injection and vulnerability detection in complex SoCs.

As digital systems are continuously becoming more complex, new methods are required to ensure their resilience. Research and industry are working together to develop automated formal methods, and, recently, great progress has been made to overcome this challenge. This work describes a general procedure to quantitatively determine, by Model Checking, the resilience level of a digital block whose flip-flops are perturbed by bit-flips. The flow relies on the formal proof, and provides a rich variety of results with much improved performance and accuracy (boost of ~ 300x and ~ 30x in the two test cases). The resilience metric is the number of distinct counterexamples provided by the formal engine, for each fault target. Failure traces are differentiated in two ways, showing on the test cases the great enhancement over simulation.

As digital systems keep miniaturizing and becoming more complex, new methods are required to ensure their fault tolerance. Research and industry are working together to automatize such task, and, recently, great progress has been made to overcome this challenge. Starting from an exhaustive reference simulation, we have a general procedure to determine, by Model Checking, the fault tolerance of flip-flops that are perturbed by bit-flip events. Assuming that the design is correctly implemented, the temporal properties are used as fault detectors, automatically generated through a re-adapted version of the open source software Goldmine. By this, we can also address circuits without explicit specification (blind blocks), using automatic assertions induced from the reference golden waveform. Properties are mainly mined inside the design, allowing to calculate by Model Checking the fault masking capacity of the addressed modules. We consider two medium sized blocks, showing results with much-improved performance and accuracy over classical simulated fault injection.