A Mechanized Theory for Microprocessor Correctness Statements

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

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

Abstract
Paper (postscript)
Bibtex entry


Abstract

Microprocessor verification has become increasingly challenging with the use of optimizations such as out-of-order execution. Because of the complexity of the implementations, a wide variety of microprocessor correctness statements have been proposed and used in verification efforts. In this work, we have mechanized a previously proposed framework for classifying these correctness statements. We have verified the relationships between the different points in the framework, and developed a characterization of the commonly used flushing abstraction function. The relationships between points in the framework are general theorems that provide ``verification highways'' to connect different correctness statements and provide reusable verification strategies. We have used these highways to determine the precise relationships between top-level correctness statements used in verification efforts.

Bibtex Entry

@TECHREPORT{DaAaLo02,
  title={A Mechanized Theory for Microprocessor Correctness Statements},
  author = {Nancy A. Day and Mark D. Aagaard and Meng Lou},
  institution = {Department of Computer Science, University of Waterloo},
  number = {2002-11},
  month = {March},
  year = 2002
}

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