Title :
HDL Program Slicing to Reduce Bounded Model Checking Search Overhead
Author :
Ou, Jen-Chieh ; Saab, Daniel G. ; Abraham, Jacob A.
Author_Institution :
Dept. of Electron. Eng. & Comput. Sci., Case Western Reserve Univ., Cleveland, OH
Abstract :
The size of the hardware description model for a complex modern digital system is increasing rapidly. CAD tools used to analyze these models are challenged by this increase in model complexity. This paper presents a technique that extracts for a given set of variables, a smaller HDL executable design slice that includes all the behavioral elements that affect those variables directly or indirectly. The design slice when compiled produces a behavior for the set of variables equivalent to the one computed by the original unsliced design. ATPG and verification tools analyzing this design could use the sliced model to reduce computation overhead. This technique was implemented in a computer program and evaluated its impact on the bounded model checker, SMV. Results show a reduction for both CPU time and memory needed by SMV to verify a publicly available model of the USB 2.0 IP core
Keywords :
automatic test pattern generation; formal verification; hardware description languages; program slicing; ATPG tools; HDL program slicing; SMV; USB 2.0 IP core; bounded model checking; digital system; hardware description model; verification tools; Application software; Automatic test pattern generation; Circuits; Data mining; Design automation; Formal verification; Hardware design languages; Jacobian matrices; Process design; Signal processing;
Conference_Titel :
Test Conference, 2006. ITC '06. IEEE International
Conference_Location :
Santa Clara, CA
Print_ISBN :
1-4244-0292-1
Electronic_ISBN :
1089-3539
DOI :
10.1109/TEST.2006.297665