Title :
Verifying Tomasulo´s algorithm by refinement
Author :
Arons, T. ; Pnueli, A.
Author_Institution :
Dept. of Appl. Math., Weizmann Inst. of Sci., Rehovot, Israel
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 :
instruction sets; integrated circuit design; microprocessor chips; processor scheduling; Tomasulo´s algorithm; dynamic scheduling; out-of-order execution; refinement; register files; sequential instruction execution algorithm; superscalar processors; Algorithm design and analysis; Computer aided instruction; Concrete; Counting circuits; Data structures; Delay systems; Law; Legal factors; Radio frequency; Registers;
Conference_Titel :
VLSI Design, 1999. Proceedings. Twelfth International Conference On
Conference_Location :
Goa
Print_ISBN :
0-7695-0013-7
DOI :
10.1109/ICVD.1999.745165
