FVP-SAT.3.0 in CNF Format ========================================================================== Author: Miroslav N. Velev mvelev@ece.cmu.edu http://www.ece.cmu.edu/~mvelev Date: March 14, 2002 Description ---------------------------- 20 satisfiable benchmarks, generated in the formal verification of buggy variants of an out-of-order superscalar processor that has 64 Reorder Buffer entries (i.e., up to 64 instructions in various stages of execution) and can fetch and retire up to 4 instructions per clock cycle. 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 ---------------------------- Each benchmark is approximately 25 MB when uncompressed with 'gunzip'.