TY - GEN
T1 - Property-specific testbench generation for guided simulation
AU - Gupta, A.
AU - Casavant, A. E.
AU - Ashar, P.
AU - Liu, X. G.
AU - Mukaiyama, A.
AU - Wakabayashi, K.
N1 - Publisher Copyright:
© 2002 IEEE.
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=4444345133&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=4444345133&partnerID=8YFLogxK
U2 - 10.1109/ASPDAC.2002.994973
DO - 10.1109/ASPDAC.2002.994973
M3 - Conference contribution
AN - SCOPUS:4444345133
T3 - Proceedings - 7th Asia and South Pacific Design Automation Conference, 15th International Conference on VLSI Design, ASP-DAC/VLSI Design 2002
SP - 524
EP - 531
BT - Proceedings - 7th Asia and South Pacific Design Automation Conference, 15th International Conference on VLSI Design, ASP-DAC/VLSI Design 2002
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 7th Asia and South Pacific Design Automation Conference, 15th International Conference on VLSI Design, ASP-DAC/VLSI Design 2002
Y2 - 7 January 2002 through 11 January 2002
ER -