A Hybrid Algorithm to Conservatively Check the Robustness of Circuits

Abstract

As systems become more complex, the size of transistors decreases. This effect leads to an increased probability of transient faults as well as higher variability of the transistors. Verifying that circuits are robust against transient faults and variability is mandatory. While formal verification may be used to prove robustness, a model that includes extracted electrical parameters and the corresponding timing information is usually too complex in practice. The contribution of this paper consists in a hybrid algorithm that can decide robustness. The algorithm uses Boolean reasoning as well as simulation to decompose the problem into feasible SAT formulas and still achieves completeness. In our experiments, we compare the algorithm against our previous implementation and achieve an average speed up of 1500 on the ISCAS-85 benchmarks and fault tolerant modifications.