SSS-SAT.1.0 in Trace Format 100 benchmarks, generated in the formal verification of buggy versions of a dual-issue superscalar microprocessor with exceptions, multicycle functional units, and branch prediction ========================================================================== 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 9, 2001 This research was supported in part by the SRC under contract 01-DC-684. Note: ----- The benchmarks are up to 0.23 MB in gzip-ed form, but up to 2.6 MB when gunzip-ed. The entire directory is 7 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, SSS-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 propositional formulas use only the following Boolean connectives: NOT, AND, OR, and ITE. They are generated according to the Trace Format [5], with _temp_977 = or(_Taken_Branch_1_1, EX_MEM_Jump, __temp_973); _temp_978 = not(_temp_977); _temp_979 = and(_temp_976, _temp_978); _temp_980 = ite(_temp_979, IF_ID_Branch, Branch_0); being examples of the Boolean connectives in the format. All the benchmarks contain a single formula to be checked for being a tautology. Since the designs are buggy, this is achieved by means of the following Trace Format commands at the end of each file: true_value = new_int_leaf(1); are_equal(_temp_1252, true_value); % 0 indicating that the formula should not be a tautology. 2. Benchmarks ------------- 2dlx_cc_mc_ex_bp_f2_bug*.trace are the Boolean conditions for the incorrectness of 100 buggy versions of a dual-issue superscalar DLX [4] microprocessor with exceptions, multicycle functional units, and branch prediction--see [2] for a description. The checking of the invariants is included in the formulas. The benchmarks contain constraints for transitivity of equality [1]. The formal verification was done as described in [3]. The formula for the formal verification of the correct processor is 2dlx_cc_mc_ex_bp_f.trace in benchmark suite FVP-UNSAT-1.0, available from http://www.ece.cmu.edu/~mvelev. 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] 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. [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. [4] J.L. Hennessy, and D.A. Patterson, Computer Architecture: A Quantitative Approach, 2nd edition, Morgan Kaufmann Publishers, San Francisco, CA, 1996. [5] B. Yang, BDD Trace Driver. Available from: http://www.cs.cmu.edu/~bwolen/software/. /**************************************************************************** * 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. * * * ****************************************************************************/