Sequential circuit diagnosis based on formal verification techniques

This paper deals with the generation of diagnostic test sequences for real-size synchronous sequential circuits. A modified fault simulator is used for assessing the diagnostic power of existing detection-oriented test patterns and a diagnostic procedure for generating new ones is described. The diagnostic procedure successfully exploits symbolic FSM equivalence proof algorithms. In order to resort to product machine traversal only when really needed, special checks are performed to verify combinational identity and identity on reachable states. As all faults are attributed to theirequivalence class, this method may be used to build a complete and exact diagnostic tree. Experimental results on ISCAS'89 circuits show the feasibility of the approach.