Sciweavers

DAC
2004
ACM

A general decomposition strategy for verifying register renaming

15 years 15 days ago
A general decomposition strategy for verifying register renaming
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 DualRAT technique, which is based on the Intel Pentium R 4 processor. Categories and Subject Descriptors
Hazem I. Shehata, Mark Aagaard
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2004
Where DAC
Authors Hazem I. Shehata, Mark Aagaard
Comments (0)