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
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
>