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...

• Type: Conference
• Year: 2009
• Where: FMCAD
• Authors: Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham
• Keywords: Abstract—Symbolic Trajectory Evaluation, FMCAD 2009, Formal Methods, Symbolic Trajectory Evaluation, Trajectory Evaluation