Name
Abstract | ||
|---|---|---|
This paper describes a strategy for verifying data-hazard correctness of out-of-order processors that implement register-renaming. We define a set of predicates to characterize register-renaming techniques and provide a set of model-checking obligations that are sufficient to guarantee that a register-renaming technique satisfies data-hazard correctness. We demonstrate how two register renaming techniques (retirement-register-file and dual-RAT) instantiate our predicates, and present model checking results for the Dual-RAT technique, which is based on the Intel Pentium 4 processor. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1145/996566.996632 | San Diego, CA, USA |
Keywords | Field | DocType |
intel pentium,general decomposition strategy,present model checking result,model-checking obligation,register-renaming technique,verifying register renaming,out-of-order processor,data-hazard correctness,dual-rat technique,registers,model checking,register file,circuits,out of order,algorithm design and analysis,data engineering,hazards,register renaming,satisfiability | Permission,Model checking,Programming language,Algorithm design,Computer science,Correctness,Parallel computing,Real-time computing,Information engineering,Pentium,Register renaming,Out-of-order execution | Conference |
ISSN | ISBN | Citations |
0738-100X | 1-58113-828-8 | 3 |
PageRank | References | Authors |
0.39 | 12 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hazem I. Shehata | 1 | 3 | 0.39 |
| Mark D. Aagaard | 2 | 119 | 8.91 |