Relating Multi-step and Single-step Microprocessor Correctness Statements

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

In Formal Methods in Computer-Aided Design, 2002.

Abstract
Paper available at Springer
Talk (.pdf.gz)
Bibtex entry

Abstract

A diverse collection of correctness statements have been proposed and used in microprocessor verification efforts. Correctness statements have evolved from criteria that match a single step of the implementation against the specification to seemingly looser, multi-step, criteria. In this paper, we formally verify conditions under which two categories of multi-step correctness statements logically imply single-step correctness statements. The first category of correctness statements compare flushed states of the implementation and the second category compare states that are able to retire instructions. Our results are applicable to superscalar implementations, which fetch or retire multiple instructions in a single step.

Bibtex Entry

@INPROCEEDINGS{AaDaLo02,
  title={Relating Multi-step and Single-step Correctness Statements},
  author ={ Mark D. Aagaard and Nancy A. Day and Meng Lou},
  booktitle={Formal Methods in Computer-Aided Design},
  series={Lecture Notes in Computer Science},
  volume=2517,
  publisher={Springer}
  editors ={Mark D. Aagaard and John W. O'Leary},
  month={November},
  year = 2002,
  pages ={123-141}
}

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