HDL Program Slicing to Reduce Bounded Model Checking Search Overhead

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