Superscalar Suite 1.0a (SSS.1.0a) in CNF Format
==========================================================================

Author:      Miroslav N. Velev
             Department of Electrical and Computer Engineering
             Carnegie Mellon University
             Pittsburgh, PA 15213, U.S.A.
             mvelev@ece.cmu.edu
             http://www.ece.cmu.edu/~mvelev

Date:        May 28, 1999

Description: 9 CNF formulas which should be satisfiable

This research was supported in part by the SRC under contract 99-DC-068.



0. Condition of Availability
----------------------------
The SSS.1.0a benchmark suite is made available, provided that any
publications that use it will list the reference:

  M.N. Velev, Superscalar Suite 1.0a. Available from: http://www.ece.cmu.edu/~mvelev.

and that the authors of such publications will email
  Miroslav N. Velev (mvelev@ece.cmu.edu)
and
  Randal E. Bryant (Randy.Bryant@cs.cmu.edu)
with the best results achieved, and with enough technical details as to enable the
replication of the experiments.



1. Format Description
---------------------
The CNF format was used.
(See ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.tex)



2. Benchmarks
-------------
The propositional formulas were generated as described in [1]. They represent
the correctness criteria for a 2-issue in-order superscalar DLX [2] processor,
which has two complete pipelines, 4 possible load interlocks, but no structural 
hazards, such that 0, 1, or 2 new instructions can be fetched each cycle.

The benchmarks dlx2_cc_a_bug* are incorrect versions of the design.
The sequence of bug numbers does not reflect the relative complexity of the
Boolean formulas.
They should all be satisfiable, i.e., there should be a counterexample for
the correctness of each buggy processor.



References:
-----------
[1] M.N. Velev, and R.E. Bryant, "Superscalar Processor Verification 
    Using Efficient Reductions of the Logic of Equality with Uninterpreted 
    Functions to Propositional Logic", Correct Hardware 
    Design and Verification Methods (CHARME'99), September 1999.
    Available from: http://www.ece.cmu.edu/~mvelev.
[2] J.L. Hennessy, and D.A. Patterson, Computer Architecture: 
    A Quantitative Approach, 2nd edition, Morgan Kaufmann Publishers, 
    San Francisco, CA, 1996.



/****************************************************************************
* Copyright (c) 1999  Carnegie Mellon University.                           * 
* All rights reserved.                                                      *
*                                                                           *
* This benchmark suite is distributed by Carnegie Mellon University         *
* ("University") under license agreement "as is" on a nonexclusive,         *
* royalty-free basis, completely without warranty or service support.       *
* This benchmark suite is for internal use only within the licensee         *
* organization, including all divisions and subsidiaries.                   *
*                                                                           *
* The University hearby disclaims all implied warranties, including the     *
* implied warranties of merchantability and fitness for a particular        *
* purpose.  The University and its employees shall not be liable for any    *
* damages incurred by the licensee in use of the benchmark suite, including *
* direct, indirect, special, incidental, or consequential damages.          *
*                                                                           *
****************************************************************************/