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
This publication has 1 reference indexed in Scilit:
- An Efficient Algorithm for Exploiting Multiple Arithmetic UnitsIBM Journal of Research and Development, 1967