1. Introduction: Special Issue on Microprocessor Verifications

   • Warren A. Hunt Jr.

   Introduction Pages: 135 - 137

2. Formal Verification of Out-of-Order Execution with Incremental Flushing

   • Robert B. Jones
   • Jens U. Skakkebæk
   • David L. Dill

   OriginalPaper Pages: 139 - 158

3. Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function

   • Sergey Berezin
   • Edmund Clarke
   • Yunshan Zhu

   OriginalPaper Pages: 159 - 186

4. Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability

   • Jun Sawada
   • Warren A. Hunt Jr.

   OriginalPaper Pages: 187 - 222