Property-specific testbench generation for guided simulation

Simulation continues to be the primary technique for functional validation of designs. It is important that simulation vectors be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The overall focus of our work is to generate a property-specific testbench for guided simulation, that is targeted either at proving the correctness of a property or at finding a bug. This is facilitated by generation of a properly-specific model, called a "witness graph", which captures interesting paths in the design. Starting from an initial abstract model of the design, symbolic model checking, pruning, and refinement steps are applied in an iterative manner, until either a conclusive result is obtained or computing resources are exhausted. This paper describes the theoretical underpinnings of generating and using a witness graph for computation tree logic (CTL) correctness properties, practical issues related to the generation of a testbench, and experiences with an industrial example. We have been able to demonstrate on a real in-house LSI design that such an approach can lead to significant reduction in the time required to analyze the design for a CTL property and find a witness