Conditioned HDL Slicing A way to Speed-up Formal Verification

Modern complex digital systems are described in Hardware Description Language (HDL). The increase in design complexity are causing verification tools to require large amount of resources. In this paper, we propose a technique to obtain a HDL executable conditioned design slice that is behaviorally equivalent to the original design. The conditioned slice is less complex than the original and static sliced design and require less resources to analyze by a verification tool. The slicer is implemented in a computer program which is used as a pre-processor to SMV verification. The results show that the conditioned slice significantly reduces the CPU and memory overhead needed to verify the USB2.0 IP core by SMV.