Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach
1999; Springer Science+Business Media; Linguagem: Inglês
10.1007/3-540-48683-6_7
ISSN1611-3349
AutoresRavi Hosabettu, Mandayam Srivas, Ganesh Gopalakrishnan,
Tópico(s)Mathematical Control Systems and Analysis
ResumoThe Completion Functions Approach was proposed in [HSG98] as a systematic way to decompose the proof of correctness of pipelined 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 instruction. In this paper, we show that this "instruction-centric" view of the completion functions approach leads to an elegant decomposition of the proof for an out-of-order execution processor with a reorder buffer. The proof does not involve the construction of an explicit intermediate abstraction, makes heavy use of strategies based on decision procedures and rewriting, and addresses both safety and liveness issues with a clean separation between them.
Referência(s)