Title :
Automated formal verification of X propagation with respect to testability issues
Author :
Dehbashi, Mehdi ; Tille, Daniel ; Pfannkuchen, Ulrike ; Eggersglus, Stephan
Author_Institution :
Inst. of Comput. Sci., Univ. of Bremen, Bremen, Germany
Abstract :
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.
Keywords :
flip-flops; formal verification; X propagation; automated formal verification; flipflops; logic built-in self-test; multiple-input signature register; scan test; Benchmark testing; Hardware; Integrated circuits; Latches; Logic gates; Registers; Timing; Dangerous X Source; Formal Verification; Observation Point; Testability;
Conference_Titel :
Design & Test Symposium (IDT), 2014 9th International
Conference_Location :
Algiers
DOI :
10.1109/IDT.2014.7038596