Tightly integrate dynamic verification with formal verification: a GSTE based approach
The work
| Authors | Jin Seok Yang; Avi Puder |
|---|---|
| Editors | |
| Type | misc |
| Year | 2005 |
| Citekey | yang2005tightly |
Where it appeared
| Published in | Asia and South Pacific Design Automation Conference (ASP-DAC) |
|---|---|
| Volume | 1 |
| Pages | 327--330 |
Identifiers
| DOI | 10.1109/aspdac.2005.1466183 |
|---|---|
| OpenAlex | W4247782789 |
Access
| Landing page | https://doi.org/10.1109/aspdac.2005.1466183 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
GSTE (generalized symbolic trajectory evaluation) is a high capacity formal verification technology that has been successfully applied to verifying complex Intel designs with tens of thousands of state elements. In this paper, we extend the use of GSTE by developing a dynamic checker that verifies a GSTE specification against a scalar simulation trace. Unlike previous approaches, both the formal checker and the dynamic checker work directly on a GSTE specification without the need for an intermediate monitor circuit. Our approach also offers a straight forward way to measure the quality (coverage) of a specification. The dynamic checker has been used in the real-life microprocessor design verification.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 21:40 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@misc{yang2005tightly,
title = {Tightly integrate dynamic verification with formal verification: a GSTE based approach},
author = {Jin Seok Yang and Avi Puder},
year = {2005},
journal = {Asia and South Pacific Design Automation Conference (ASP-DAC)},
volume = {1},
pages = {327--330},
doi = {10.1109/aspdac.2005.1466183},
}
This record lives at https://refs.drheap.org/yang2005tightly/ and will keep doing so.