A proof of correctness of a processor implementing tomasulo's algorithm without a reorder buffer

摘要

The Completion Functions Approach was proposed in [HSG98] as a systematic way to decompose the proof of correctness of pipleined microprocessors. The central idea is to construct the abstraction function using completion functions, one per unfinished instruction, each of which specifies the effect (on the observables) of completing the instrucion. However, its applicability depends on the fact that the implementation "commits" the unfinished instructions in the pipeline in program order. In this paper, we extend the completion functions approach when this is not true and demonstrate it on an implementatin of Tomasulo's algorithm without a reorder buffer. The approach leads to an elegant decomposition of the proof of the ocrrectness criterion, does not involve the constrcution of an explicit intermediate abstraction, makes heavy use of an automatic case-analysis strategy based on decision procedures and rewriting, and addresses both safety and liveness issues.