Complementary Formal Approaches for Dependability Analysis

Evaluating the robustness of digital circuits with respect to soft errors has become an important part of the design flow for many applications. The identification of the most or less critical registers is often necessary, in order to reach the lowest overheads while achieving a given application-level robustness. The goal here is to identify those soft errors actually harmful for the system, not to compute the Soft Error Rate. In this context, we investigate new approaches based on formal techniques to improve design-time robustness evaluations at least for the most critical blocks in a circuit. Preliminary results are shown, focusing on the evaluation of self-healing (or self-repairing) capabilities.