Verifying Tomasulo's algorithm by refinement

1 January 1999

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

No. 10639667,p. 306-309
https://doi.org/10.1109/icvd.1999.745165

Abstract

In this paper Tomasulo's algorithm for out-of-order execution is shown to be a refinement of the sequential instruction execution algorithm. Correctness of Tomasulo's algorithm is established by proving that the register files of Tomasulo's algorithm and the sequential algorithm agree once all instructions have been completed.

Keywords

COUNTING CIRCUITS
CONCRETE
LAW
LEGAL FACTORS
ALGORITHM DESIGN AND ANALYSIS
REGISTERS
DELAY SYSTEMS
COMPUTER AIDED INSTRUCTION
RADIO FREQUENCY
DATA STRUCTURES

This publication has 1 reference indexed in Scilit:

An Efficient Algorithm for Exploiting Multiple Arithmetic Units
IBM Journal of Research and Development, 1967

Cited by 12 articles