Due to their shrinking feature sizes as well as environmental influences, such as high-energy radiation, electrical noise, and particle strikes, integrated circuits are getting more vulnerable to transient faults. Accordingly, how to make those circuits more robust has become an essential step in today's design flows. Methods increasing the robustness of circuits against these faults already exist for a long period of time but either introduce huge additional logic, change the timing behavior of the circuit, or are applicable for dedicated circuits such as microprocessors only. In this paper, we propose an alternative method, which overcomes these drawbacks by determining application-specific knowledge of the circuit, namely the relations of flip-flops and when they assume the same value. By this, we exploit partial redundancies, which are inherent in most circuits anyway (even the optimized ones), to frequently compare the circuit signals for their correctness-eventually leading to an increased robustness. Since determining the correspondingly needed information is a computationally hard task, formal methods, such as bounded model checking, satisfiability-based automatic test pattern generation, and binary decision diagrams, are utilized for this purpose. The resulting methodology requires only a slight increase in additional hardware, does only influence the timing behavior of the circuit negligibly, and is automatically applicable to arbitrary circuits. Experimental evaluations confirm these benefits.

Due to shrinking feature sizes, integrated circuits are getting more vulnerable against transient faults. Methods increasing the robustness of circuits against these faults already exist for a long period of time but either introduce huge additional logic, increase the latency of the circuit, or are applicable for dedicated circuits such as microprocessors only. This work proposes an alternative hardening method which requires only a slight increase in additional hardware, does not influence the timing behavior, and is automatically applicable to arbitrary circuits. To this end, application-specific knowledge of the considered circuit is exploited, analyzed by a dedicated orchestration of formal techniques, and, eventually, used to synthesize a fault detection mechanism enhancing the robustness of the circuit. Experimental evaluations show that the proposed solution leads to a significant increase in the robustness, while the hardware overhead is kept moderate.

Embedded systems consist of hardware and software and are ubiquitous in safety-critical and mission-critical fields. The increasing integration density of modern, digital circuits causes an increasing vulnerability of embedded systems to transient faults. Techniques to improve the fault tolerance are often either implemented in hardware or in software. In this paper, we focus on synthesis techniques to improve the fault tolerance of embedded systems considering hardware and software. A greedy algorithm is presented which iteratively assesses the fault tolerance of a processor-based system and decides which components of the system have to be hardened choosing from a set of existing techniques. We evaluate the algorithm in a simple case study using a Traffic Collision Avoidance System (TCAS).

Continuously shrinking feature sizes result in an increasing susceptibility of circuits to transient faults, e.g., due to environmental radiation. Approaches to implement fault tolerance are known. But assessing the fault tolerance of a given implementation is a hard verification problem. Here, we propose the use of formal methods to assess the robustness of a digital circuit with respect to transient faults. Our formal model uses a fixed bound in time and exploits fault detection circuitry to cope with the complexity of the underlying sequential equivalence check. As a result, a lower and an upper bound on the robustness are returned together with vulnerable components. The underlying algorithm and techniques to improve the efficiency are presented. In experiments, we evaluate the method on circuits with different fault detection mechanisms.

In presence of increasing soft error rates due to shrinking feature sizes, design tools are required to analyze fault tolerance and robustness of circuits. Here, we propose a new measure that identifies hot-spots in the design. On the one hand the measure is more accurate than a "worst-case analysis" that ignores excitation probabilities. On the other hand the computation of the new measure is more efficient than a "probabilistic analysis" that considers excitation probabilities at the cost of a higher computational complexity. Both of these extremes can be embedded in the new measure. Experimental results on circuits with protection against soft errors show that the new measure can be calculated effectively.

Continuously shrinking feature sizes cause an increasing vulnerability of digital circuits. Manufacturing failures and transient faults may tamper the functionality. Automated support is required to analyze the fault tolerance of circuits. In this paper, Robu Check is presented - a design tool to analyze the fault tolerance of digital circuits. Engines based on simulation and formal methods are integrated to identify components that require additional fault protection. Consequently, an overall estimation of fault tolerance of the circuit is determined.

Researchers are looking for alternatives to overcome the upcoming limits of conventional hardware technologies. Reversible logic thereby established itself as a promising direction so that several methods for synthesis, verification, and testing of reversible circuits have already been proposed. However, also methods for debugging, i.e., to determine error candidates in case of a failed verification, are required to complete the design flow. Even if first approaches have already been proposed, debugging of reversible circuits still is in the beginning. In this paper, we present an alternative method to automatically debug reversible circuits. We thereby focus on missing control errors -- an established error model in the design of reversible circuits. A new notion of an error candidate is proposed that relies on the observation of a necessary condition for error locations in reversible circuits. Using this notion, a set of error candidates is obtained that differs from the error candidates returned by previous methods. Thus, combining the approaches enhances the overall debugging flow. Experimental results demonstrate that a higher accuracy is obtained in significantly shorter run-time.

Intensive research is performed to find post-CMOS technologies. A very promising direction based on reversible logic are quantum computers. While in the domain of reversible logic synthesis, testing, and verification have been investigated, debugging of reversible circuits has not yet been considered. The goal of debugging is to determine gates of an erroneous circuit that explain the observed incorrect behavior. In this paper we propose the first approach for automatic debugging of reversible Toffoli networks. Our method uses a formulation for the debugging problem based on Boolean satisfiability. We show the differences to classical (irreversible) debugging and present theoretical results. These are used to speed-up the debugging approach as well as to improve the resulting quality. Our method is able to find and to correct single errors automatically.

Feature sizes in VLSI circuits are steadily shrinking. This results in increasing susceptibility to soft errors, e.g. due to environmental radiation. Precautions against soft errors can be taken on all design stages, e.g. the architectural level, algorithmic level, or on the layout level. Whether the final implementation contains flaws or really provides robustness to soft errors remains to be checked. Here, we propose an approach to formally verify the robustness of a circuit with respect to multiple soft errors. We propose a fault model that prunes the exponentially sized space of multiple soft errors and an algorithm that automatically analyzes a given circuit.