Cross-fertilizing FSM verification techniques and sequential diagnosis

The authors present a technique for assessing the diagnostic power of an existing detection-oriented test pattern by means of diagnostic fault simulation and a procedure to improve it. The procedure successfully exploits enhanced symbolic finite state machine (FSM) equivalence proof algorithms. In order to resort to product machine traversal only when needed, special checks are performed to verify combinational identity and identity on reachable states. As all faults are attributed to their equivalence class, this method may be used to build a complete and exact diagnostic tree. Experimental results support the claim that the diagnosis of real-world synchronous sequential circuits has become feasible for the first time