Benchmarks in ISCAS-CGRASP [5] 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:        February 7, 2001

Description: Propositional logic formulas generated as described in [3].
             If the output 'out' is satisfiable then there is a counterexample
             for the correctness of the microprocessor, i.e., it is incorrect.

This research was supported in part by the SRC under contract 00-DC-684.


NOTE: The difference between the ISCAS-CGRASP [5] and ISCAS [4] formats
      is that constraints for transitivity of equality [1][2] are 
      included as comments in the former but are part of the formula
      in the latter.
      However, the constraints still need to be considered if the ISCAS-CGRASP
      formula is checked for satisfiability, i.e., a satisfying assignment
      should also satisfy all the constraints in order to be a valid
      counterexample.



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

  M.N. Velev, <benchmark suite name>, Available from: http://www.ece.cmu.edu/~mvelev.

Please let us know the best results that you achieve:
  Miroslav N. Velev (mvelev@ece.cmu.edu)
  Randal E. Bryant  (Randy.Bryant@cs.cmu.edu)



1. Format Description
---------------------
The propositional formulas use the following Boolean connectives:
NOT, AND, and OR. Comments begin with '#'.






References:
-----------
[1] R.E. Bryant, and M.N. Velev, "Boolean Satisfiability with Transitivity 
    Constraints," Computer-Aided Verification (CAV '00), E.A. Emerson and 
    A.P. Sistla, eds., LNCS 1855, Springer-Verlag, July 2000, pp. 86-98.
[2] R.E. Bryant, and M.N. Velev, "Boolean Satisfiability with Transitivity 
    Constraints," Technical Report CMU-CS-00-101, Carnegie Mellon University, 2000.
[3] 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.
[4] ISCAS85 format, http://www.cbl.ncsu.edu/CBL_Docs/iscas85.html
[5] CGRASP, http://vinci.inesc.pt/cgrasp/  
    and http://sat.inesc.pt/~jpms/research/software.html.


/****************************************************************************
* Copyright (c) 2001  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.          *
*                                                                           *
****************************************************************************/