In this paper we propose a methodology for the deductive verification of out-of-order scheduling algorithms. A `top-down' scheme for the systematic definition of system invariants is defined. The complementary use of predicted values, auxiliary fields storing a dispatch time prediction of an instruction's value, is proposed as a means of further simplifying the verification of systems in this class. We illustrate the use of the `top-down' methodology and predicted values in the verification of three out-of-order scheduling algorithms, including a detailed discussion of the verification of a model based on the Mips R10000.
Technical Report