Sciweavers

Share
FMCAD
2009
Springer

Assume-guarantee validation for STE properties within an SVA environment

10 years 1 months ago
Assume-guarantee validation for STE properties within an SVA environment
Abstract—Symbolic Trajectory Evaluation is an industrialstrength verification method, based on symbolic simulation and abstraction, that has been highly successful in data path verification, especially microprocessor execution units. These correctness results are typically obtained under certain assumptions about how the verified hardware block’s inputs are driven, as well as assumptions about the values of these inputs. For correct overall operation, the hardware environment within which the verified block resides is expected to satisfy these assumptions. We describe a translation of these proof assumptions into System Verilog Assertions. These are then used as checkers in dynamic validation of the hardware environment within which blocks verified by Symbolic Trajectory Evaluation operate. The result is a pragmatic assume-guarantee method that increases the quality and confidence in verification results, requires little or no modification to the Symbolic Trajectory Evaluat...
Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where FMCAD
Authors Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham
Comments (0)
books