1999 | OriginalPaper | Buchkapitel
Formal Verification of Explicitly Parallel Microprocessors
verfasst von : Byron Cook, John Launchbury, John Matthews, Dick Kieburtz
Erschienen in: Correct Hardware Design and Verification Methods
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The trend in microprocessor design is to extend instruction-set architectures with features—such as parallelism annotations, predication, speculative memory access,or multimedia instructions—that allow the compiler or programmer to express more instruction-level parallelism than the microarchitecture is willing to derive. In this paper we show how these instruction-set extensions can be put to use when formally verifying the correctness of a microarchitectural model. Inspired by Intel’s IA-64, we develop an explicitly parallel instruction-set architecture and a clustered microarchitectural model. We then describe how to formally verify that the model implements the instruction set. The contribution of this paper is a specification and verification method that facilitates the decomposition of microarchitectural correctness proofs using instruction-set extensions.