A Basis for Formal Robustness Checking

Correct input/output behavior of circuits in presence of internal malfunctions becomes more and more important. But reliable and efficient methods to measure this robustness are not available yet. In this paper a formal measure for the robustness of a circuit is introduced. Then, a first algorithm to determine the robustness is presented. This is done by reducing the problem either to sequential equivalence checking or to a sequence of property checking instances. The technique also identifies those parts of the circuit that are not robust from a functional point of view and therefore have to be hardened during layout.