VLIW-SAT.1.0 in CNF Format 100 satisfiable CNF benchmarks, generated in the formal verification of buggy versions of a VLIW microprocessor. ========================================================================== 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: October 10, 2000 This research was supported in part by the SRC under contract 00-DC-684. Note: ----- Each of the benchmarks is between 0.9 and 1.5 MB in gzip-ed form, and up to 6 MB when gunzip-ed. The entire directory is 114 MB. 0. Condition of Availability ---------------------------- The benchmark suite is made available, provided that any publications that use it will list the reference: M.N. Velev, VLIW-SAT.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 ------------- 9vliw_bp_mc_bug*.cnf are the Boolean conditions for the correctness of 100 (buggy) versions 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 benchmarks contain constraints for transitivity of equality [2]. The formal verification was done as described in [3]. The formula for the formal verification of the correct processor is 9vliw_bp_mc.cnf in benchmark suite FVP-UNSAT-1.0, available from http://www.ece.cmu.edu/~mvelev. 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, "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. /**************************************************************************** * 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. * * * ****************************************************************************/