Title
Verifying Tomasulo's algorithm by refinement
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.
Year
DOI
Venue
1999
10.1109/ICVD.1999.745165
VLSI Design
Keywords
Field
DocType
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
Instruction set,Computer science,Parallel computing,Correctness,Algorithm,Real-time computing,Tomasulo algorithm,Register renaming,Sequential algorithm,Out-of-order execution,Re-order buffer,Reservation station
Conference
ISSN
ISBN
Citations 
1063-9667
0-7695-0013-7
17
PageRank 
References 
Authors
1.14
4
2
Name
Order
Citations
PageRank
Tamarah Arons127814.59
Amir Pnueli2129642377.59