Name
Abstract | ||
|---|---|---|
. This paper presents several techniques for formally verifyingpipelined microprocessor implementations that contain out-of-orderexecution and dynamic resolution of data-dependent hazards. Our principaltechnique models the trace of executed instructions using a tablebasedrepresentation called a MAETT. We express invariant propertiesof pipelined implementations by specifying relations between fields inthe MAETT. To show the viability of this technique, we have proved thecorrectness ... |
Year | DOI | Venue |
|---|---|---|
1997 | 10.1007/3-540-63166-6_36 | CAV |
Keywords | Field | DocType |
trace table,pipeline microprocessor verification | Programming language,Computer science,Correctness,Implementation,Execution unit,ACL2,Distributed computing,Trace table,Automated theorem proving,Parallel computing,Microprocessor,Register file,Algorithm | Conference |
Volume | ISSN | ISBN |
1254 | 0302-9743 | 3-540-63166-6 |
Citations | PageRank | References |
40 | 4.50 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jun Sawada | 1 | 325 | 21.16 |
| Warren A. Hunt, Jr. | 2 | 520 | 59.18 |