Untestable Fault Identification in Sequential Circuits Using Model-Checking

Similar to test pattern generation, the problem of identifying untestable faults in sequential synchronous circuits remains unsolved. The previously published works in untestability identification operate at the logic-level and, thus, they do not scale with the increasing complexity of modern designs. Current paper proposes applying model-checking for detecting untestable stuck-at faults at the register-transfer level. In particular, we present a method of generating PSL language assertions for proving untestable register stuck-on faults. Experiments show that the faults identified by the method form in fact a large subset of all the untested stuck-at faults. An additional application of the method is in high-level test synthesis, where testability of sequential designs can be improved simultaneously with minimization of the circuit area. Furthermore, identification of untestable gate-level faults from RT-level can contribute to avoiding over testing and to reducing yield loss.