DocumentCode
2552692
Title
Verifying Tomasulo´s algorithm by refinement
Author
Arons, T. ; Pnueli, A.
Author_Institution
Dept. of Appl. Math., Weizmann Inst. of Sci., Rehovot, Israel
fYear
1999
fDate
7-10 Jan 1999
Firstpage
306
Lastpage
309
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;
fLanguage
English
Publisher
ieee
Conference_Titel
VLSI Design, 1999. Proceedings. Twelfth International Conference On
Conference_Location
Goa
ISSN
1063-9667
Print_ISBN
0-7695-0013-7
Type
conf
DOI
10.1109/ICVD.1999.745165
Filename
745165
Link To Document