TY - JOUR
T1 - Property-specific witness graph generation for guided simulation
AU - Casavant, A.
AU - Gupta, A.
AU - Liu, S.
AU - Mukaiyama, A.
AU - Wakabayashi, K.
AU - Ashar, P.
PY - 2001/1/1
Y1 - 2001/1/1
N2 - A practical solution to the complexity of design validation is semi-formal verification, where the specification of correctness criteria is done formally, as in model checking, but checking is done using simulation, which is guided by directed vector sequences derived from knowledge of the design and/or the property being checked. Simulation vectors must be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The focus of our work is to generate property-specific testbenches for guided simulation, that are targeted either at proving the correctness of a full CTL property or at finding a bug. This is facilitated by generation of a property-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. The witness graph is annotated with, e.g., state or transition priorities before testbench generation. The overall testbench generation flow, and the iterative flow for witness graph generation are shown.
AB - A practical solution to the complexity of design validation is semi-formal verification, where the specification of correctness criteria is done formally, as in model checking, but checking is done using simulation, which is guided by directed vector sequences derived from knowledge of the design and/or the property being checked. Simulation vectors must be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The focus of our work is to generate property-specific testbenches for guided simulation, that are targeted either at proving the correctness of a full CTL property or at finding a bug. This is facilitated by generation of a property-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. The witness graph is annotated with, e.g., state or transition priorities before testbench generation. The overall testbench generation flow, and the iterative flow for witness graph generation are shown.
UR - http://www.scopus.com/inward/record.url?scp=84893676296&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84893676296&partnerID=8YFLogxK
U2 - 10.1109/DATE.2001.915124
DO - 10.1109/DATE.2001.915124
M3 - Article
AN - SCOPUS:84893676296
SN - 1530-1591
JO - Proceedings -Design, Automation and Test in Europe, DATE
JF - Proceedings -Design, Automation and Test in Europe, DATE
M1 - 915124
ER -