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.
Citation:
Tamarah Arons, Amir Pnueli, "Verifying Tomasulo's Algoithm by Refinement," vlsid, pp.306, 12th International Conference on VLSI Design - 'VLSI for the Information Appliance', 1999 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||