Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction
The work
| Authors | Miroslav N. Velev; Randal E. Bryant |
|---|---|
| Editors | |
| Type | misc |
| Year | 2000 |
| Citekey | velev2000formal |
Where it appeared
| Published in | Proceedings - ACM IEEE Design Automation Conference |
|---|---|
| Publisher | Association for Computing Machinery |
| Pages | 112--117 |
Identifiers
| DOI | 10.1145/337292.337331 |
|---|---|
| OpenAlex | W2110011370 |
Access
| Landing page | https://doi.org/10.1145/337292.337331 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/337292.337331 |
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
We extend the Burch and Dill flushing technique [6] for formal verification of microprocessors to be applicable to designs where the functional units and memories have multicycle and possibly arbitrary latency. We also show ways to incorporate exceptions and branch prediction by exploiting the properties of the logic of Positive Equality with Uninterpreted Functions [4][5]. We study the modeling of the above features in different versions of dual-issue superscalar processors.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 11:04 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{velev2000formal,
title = {Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction},
author = {Miroslav N. Velev and Randal E. Bryant},
year = {2000},
journal = {Proceedings - ACM IEEE Design Automation Conference},
publisher = {Association for Computing Machinery},
pages = {112--117},
doi = {10.1145/337292.337331},
}
This record lives at https://refs.drheap.org/velev2000formal/ and will keep doing so.