In this paper Tomasulo's algorithm for outoforder 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.
12th International Conference on VLSI Design
PVS dump file
The
PVS dump file
consists of the follwing.
The Tomasulo system is in file Tomasulo.pvs, its invariants are
defined in TomDefs.pvs and the lemmas are listed in TomInvs.pvs
The sequential system in is file seq.pvs.
The refinement between the two files in is file TomRefinesSeq.pvs
The files def.pvs, Tdef.pvs and more_nat_types.pvs include definitions
used by the two systems.
The verification was carried out in PVS Version 2.1 (patch level 2.414)
Please refer any queries to Tamarah.