Title :
Case study of ATPG-based bounded model checking: verifying USB2.0 IP core
Author :
Qiang, Qiang ; Chang, Chia-Lun ; Saab, Daniel G. ; Abraham, Jacob A.
Author_Institution :
Electr. Eng. & Comput. Sci., Case Western Reserve Univ., Cleveland, OH, USA
Abstract :
This paper presents the ATPG performances of verifying USB2.0 IP core. Using the USB protocol and typical properties, the ATPG-based bounded model checking mechanism is revealed. Heuristics to accelerate the ATPG search are presented and their impacts are analyzed. We feel that results from this case study are applicable to serial communication circuits of the same family and can be scaled to industrial-sized circuits.
Keywords :
automatic test pattern generation; fault diagnosis; formal verification; logic testing; peripheral interfaces; ATPG-based bounded model checking; USB protocols; USB2.0 IP core verification; automatic test pattern generation; industrial-sized circuits; serial communication circuits; Automatic test pattern generation; Circuit faults; Computer aided software engineering; Computer science; Decision making; Jacobian matrices; Logic; Protocols; Sequential circuits; Universal Serial Bus;
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 2005. ICCD 2005. Proceedings. 2005 IEEE International Conference on
Print_ISBN :
0-7695-2451-6
DOI :
10.1109/ICCD.2005.36
