Assume-Guarantee Validation for STE Properties within an SVA Environment
The work
| Authors | Zurab Khasidashvili; Gavriel Gavrielov; Tom Melham |
|---|---|
| Editors | Armin Biere; Carl Pixley |
| Type | inproceedings |
| Year | 2009 |
| Citekey | khasidashvili2009assumeguarantee |
Where it appeared
| Published in | Formal Methods in Computer-Aided Design (FMCAD 2009) |
|---|---|
| Publisher | IEEE |
| Pages | 108--115 |
Identifiers
| DOI | 10.1109/fmcad.2009.5351133 |
|---|
Access
| Landing page | https://www.cs.ox.ac.uk/tom.melham/pub/Khasidashvili-2009-AGV.pdf |
|---|
Related
| Distinct from | aagaard1999are |
|---|---|
| Distinct from | bryant1990ternary |
| Distinct from | chakraborty2015wordlevel |
| Distinct from | kumar2023pragmatic |
| Distinct from | nukala2024translating |
| Distinct from | oleary1999formally |
| Distinct from | oleary2013relational |
From bibtex.
Abstract
Symbolic Trajectory Evaluation is an industrial-strength 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 Evaluation proofs, and leverages pre-existing dynamic validation infrastructure.
A copy is held
pdf, 220.1 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-16 23:22 UTC |
| Approved by | a person 2026-09-17 17:07 UTC |
Cite it as
@inproceedings{khasidashvili2009assumeguarantee,
title = {Assume-Guarantee Validation for STE Properties within an SVA Environment},
author = {Zurab Khasidashvili and Gavriel Gavrielov and Tom Melham},
editor = {Armin Biere and Carl Pixley},
year = {2009},
booktitle = {Formal Methods in Computer-Aided Design (FMCAD 2009)},
publisher = {IEEE},
pages = {108--115},
doi = {10.1109/fmcad.2009.5351133},
}
This record lives at https://refs.drheap.org/khasidashvili2009assumeguarantee/ and will keep doing so.