A framework for superscalar microprocessor correctness statements |
| |
| Authors: | Mark D Aagaard Byron Cook Nancy A Day Robert B Jones |
| |
| Affiliation: | (1) Electrical and Computer Engineering, University of Waterloo, Waterloo, Ontario, Canada E-mail: m.aagaard@ece.uwaterloo.ca, CA;(2) Prover Technology, Portland, Ore., USA; E-mail: byron@prover.com, US;(3) Computer Science, University of Waterloo, Waterloo, Ontario, Canada; E-mail: nday@cs.uwaterloo.ca, CA;(4) Strategic CAD Labs, Intel Corporation, Hillsboro, Ore., USA; E-mail: rjones@ichips.intel.com, US |
| |
| 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 properties
of superscalar microprocessors. Our framework is independent of the implementation representation and verification approach,
and is parameterized by the width of the processor. We characterize the relationships between the correctness statements of
many different efforts and also illustrate how classical approaches to microprocessor verification fit within our framework.
Published online: 17 December 2002 |
| |
| Keywords: | : Microprocessor correctness – Commuting diagrams – Formal verification – Pipelines |
| 本文献已被 SpringerLink 等数据库收录！ |
|
