A Formal Analysis of the Will-Retire Correctness Statement

Nancy A. Day, Mark D. Aagaard, and Meng Lou

Technical Report 2002-14, Department of Computer Science, University of Waterloo, March, 2002.

Abstract
Paper (postscript)
Bibtex entry

Abstract

We relate two microprocessor correctness statements and show that they are equivalent. The first correctness statement in question uses synchronization at retirement over a series of steps of the implementation and external equality as the required correspondence between states. The second correctness statement is the classic single-step commuting diagram with external equality as the match. We prove that if any microprocessor implementation and specification are shown to satisfy one of these correctness statements, they also satisfy the other correctness statement. This technical report is a continuation of Technical Report 2002-11 and includes little introductory material.

Bibtex Entry

@TECHREPORT{DaAaLo02,
  title={A Formal Analysis of the Will-Retire Correctness Statement},
  author = {Nancy A. Day and Mark D. Aagaard and Meng Lou},
  institution = {Department of Computer Science, University of Waterloo},
  number = {2002-14},
  month = {March},
  year = 2002
}

Send questions or comments to Mark Aagaard < markaa@swen.uwaterloo.ca >