Top-level Refinement in Processor Verification

1998.

Cited by: 2|Bibtex|Views1|
Keywords:
out of order execution

Abstract:

We provide a framework for the specification and verificationof high-performance processors. As an example, we give a high-levelspecification and correctness proof for a processor that uses speculation,register renaming, superscalar out-of-order execution, and resolution ofmemory dependencies. The specifications of its three concurrently...More

Code:

Data:

Your rating :
0

 

Tags
Comments