12th International Conference on VLSI Design - 'VLSI for the Information Appliance'
Verifying Tomasulo's Algoithm by Refinement
Goa, India
January 10-January 13
ISBN: 0-7695-0013-7
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.