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

• Type: Conference
• Year: 2004
• Where: DAC
• Authors: Hazem I. Shehata, Mark Aagaard
• Keywords: DAC 2004, Design Automation, Intel Pentium, Register Renaming Techniques, Satisfies Data-hazard Correctness