A Framework for Superscalar
Microprocessor Correctness Statements
Mark D. Aagaard, Byron Cook, Nancy A. Day, and Robert B. Jones
International Journal on Software Tools for Technology Transfer,
Springer Verlag, online publication: Dec 17, 2002.
Abstract
Most verifications of superscalar, out-of-order
microprocessors compare state-machine-based implementations and
specifications, where the specification is based on the
instruction-set architecture. The different efforts use a
variety of correctness statements, implementations, and verification
approaches.
We present a framework for classifying correctness
statements about safety
that is independent of implementation representation and
verification approach, and parameterized by the width
of the processor. We characterize the relationships between the
different statements and illustrate how existing and classical approaches
fit within this framework.
Send questions or comments to Mark Aagaard
< markaa@swen.uwaterloo.ca
>