Formal Temporal Characterization of Register Vulnerability in Digital Circuits

With the complexity of new technologies growing extremely fast over time, innovative strategies are required to verify their robustness in relatively exiguous temporal scales. Thanks to the progress of calculus power and the increasing availability of computational resources, automated formal methods are nowadays advanced enough to address this task, providing outcomes of high quality and precision in a feasible time. This paper presents a general mathematical model to quantitatively identify the most fault-sensitive regions (in both time and space) of hardware digital blocks. Error injection, propagation and detection are performed by combining the efficiency of model checking and the versatility of simulation, achieving beyond commonly obtained results on the test cases of application.