FVP-UNSAT.3.0 in CNF Format
==========================================================================

Author:      Miroslav N. Velev
             mvelev@ece.cmu.edu
             http://www.ece.cmu.edu/~mvelev

Date:        March 12, 2002


Description
----------------------------
Six unsatisfiable benchmarks, generated in the formal verification of 
out-of-order superscalar processors that have 64 Reorder Buffer entries
(i.e., up to 64 instructions in various stages of execution) and can
fetch and retire up to N instructions per clock cycle, 
where N = 1,2,4,8,16,32.

Only register-register ALU instructions are executed.
The processors do not implement register renaming. Data dependencies are 
satisfied by stalling a dependent instruction until its data operands can
be either forwarded from preceding entries in the Reorder Buffer, or
read directly from the Register File.


Conditions of Availability
----------------------------
1. Email Miroslav (mvelev@ece.cmu.edu) about any papers that you publish
   and that use these benchmarks.

2. In any publication that uses these benchmarks, reference the paper 
   that describes how the benchmarks were generated:

   M.N. Velev, "Using Rewriting Rules and Positive Equality to 
   Formally Verify Wide-Issue Out-Of-Order Microprocessors with a 
   Reorder Buffer," Design, Automation and Test in Europe (DATE '02), 
   March 2002, pp. 28-35. 


Note
----------------------------
The benchmarks are between 25 MB and 94 MB, have between 40,000 and
96,000 CNF variables, and between 1,200,000 and 4,400,000 clauses.