Taming the Complexity of STE-based Design Verification Using Program Slicing

This paper presents the development of a hierarchical methodology for speeding-up a symbolic trajectory evaluation (STE) based verification flow, using "program slicing" techniques. An overview of the proposed methodology is described, along with the details of a prototype tool that has been developed to automate the approach. The tool, called FACTOR, has been successfully applied to reduce the size of the RTL implementation of a floating-point unit in an Intelreg Pentiumreg 4 processor model needed for formally verifying an embedded module. The existing proof specification for the module was validated using Forte, Intel\´s STE tool, on both the original and the reduced model. A comparison of the results demonstrates the effectiveness of the methodology, and its immense potential to scale up the verification flow to larger design sizes