FVP-UNSAT.1.0 in CNF Format

Unsatisfiable benchmarks, generated in the formal verification of 
superscalar and VLIW processors.
==========================================================================

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:        July 26, 2000

Description: 4 CNF formulas (3 very challenging ones) that should be unsatisfiable

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



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

  M.N. Velev, FVP-UNSAT.1.0. 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
-------------
1dlx_c_mc_ex_bp_f.cnf is the Boolean condition for the correctness of 
a single-issue pipelined DLX processor [5] with multicycle functional units, 
exceptions, and branch prediction, as formally verified in [3]. The evaluation 
of the same formula with BDDs takes 6 seconds of CPU time.

2dlx_ca_mc_ex_bp_f.cnf is the Boolean condition for the correctness of
a dual-issue superscalar version of the above processor with one complete
pipeline and a second pipeline capable of executing only register-register
and register-immediate instructions. The evaluation of the same formula with 
BDDs takes 980 seconds of CPU time.

2dlx_cc_mc_ex_bp_f.cnf same as above, but the processor has two complete
pipelines. The evaluation of the same formula with BDDs takes 2,670 seconds 
of CPU time.

9vliw_bp_mc.cnf is the Boolean condition for the correctness of a 9-wide
VLIW processor with branch prediction and multicycle functional units [1]
that imitates the Intel Itanium in speculative features such as predicated
execution, register remapping, and advanced loads. The evaluation of the same 
formula with BDDs takes 113,640 seconds (31:30 hours) of CPU time.

The benchmarks do not contain constraints for transitivity of equality [2].
The formal verification was done as described in [4].

All BDD-based experimrnts were performed on a 336 MHz SUN4.


NOTE:
-----
2dlx_ca_mc_ex_bp_f.cnf, 2dlx_cc_mc_ex_bp_f.cnf, and 9vliw_bp_mc.cnf should be
very challenging for SAT-checkers.



References:
-----------

[1] M.N. Velev, Formal Verification of VLIW Microprocessors with Speculative 
    Execution, Computer-Aided Verification (CAV'00), E.A. Emerson and 
    A.P. Sistla, eds., LNCS 1855, Springer-Verlag, July 2000, pp. 296-311 

[2] 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. 

[3] M.N. Velev, and R.E. Bryant, Formal Verification of Superscalar 
    Microprocessors with Multicycle Functional Units, Exceptions, and 
    Branch Prediction, 37th Design Automation Conference (DAC '00), 
    June 2000, pp. 112-117. 

[4] 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.

[5] J.L. Hennessy, and D.A. Patterson, Computer Architecture: 
    A Quantitative Approach, 2nd edition, Morgan Kaufmann Publishers, 
    San Francisco, CA, 1996.



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