Formal Verification of Out-of-Order Execution Using Incremental Flushing

Abstract

We present a two-part approach for verifying out-of-order execution. First, the complexity of out-of-order issue and scheduling is handled by creating an in-order abstraction of the out-of-order execution core. Second, incremental flushing addresses the complexity difficulties encountered by automated abstraction functions on very deep pipelines. We illustrate the techniques on a model of a simple out-of-order processor core.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1998
Accession Number
ADA400401

Entities

People

  • David L. Dill
  • Jens U. Skakkebaek
  • Robert B. Jones

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Computers
  • Computing System Architectures
  • Content Addressable Memory
  • Digital Signal Processing
  • Instruction Set Architecture
  • Instructions
  • Microarchitecture
  • Pipelines
  • Scheduling (Production)
  • Sequences
  • Signal Processing
  • Simulations
  • Verification

Fields of Study

  • Computer science

Readers

  • Parallel and Distributed Computing.
  • Systems Analysis and Design