Bounded fault tolerance checking

Summary form only given. Continuously shrinking feature sizes result in an increasing susceptibility of circuits to transient faults. Approaches to implement fault tolerance are known e.g. on architecture level, algorithmic level, or layout level. But assessing the fault tolerance of a given circuit is a hard verification problem. Verification of the fault tolerance based on simulation is fast, but cannot cover the complete input space in combination with all potential faults in reasonable time. In contrast, formal methods are complete by proving the fault tolerance with respect to the whole input space, but may suffer from run time limitations. Here, we propose a formal model to assess the robustness of a digital circuit with respect to transient faults. Our formal model uses a fixed bound in time to cope with the complexity of the underlying Sequential Equivalence Check (SEC). Exact bounds for the robustness are retrieved while restricting the formal analysis to an observation window of t^d time steps.