Automated formal verification of X propagation with respect to testability issues

X values may be captured by scan flipflops during the scan test. An X value corrupts the signature generated by a Multiple-Input Signature Register (MISR). The MISR is used in the test structures such as Logic Built-in Self-Test (LBIST). In this paper, we propose an approach to automate formal verification of X propagation with respect to testability issues. The propagation of an X value from X sources to scan flipflops is comprehensively evaluated using formal verification considering all possible test patterns. The approach is utilized to find root causes of a corrupted signature generated by MISR and to rectify the erroneous behavior of a design because of dangerous X sources.