These AIGER models have been synthesized from the BTOR benchmarks provided by Jori Dubrovin with 'synthebtor' with versions: Boolector Version 1.5.111 c0198838eaf229382a5ca41259d5f2aec900e0b2 Lingeling Version ajt 9fae11c418eedc5f05fee833a2667a2f34e36c94 What follows below is the original README from Jori. Armin ----------------------------------------------------------------------------- Archive beem-btor version 001 date 2012-04-11 Author: Jori Dubrovin Aalto University Department of Information and Computer Science jori.dubrovin@aalto.fi This archive contains the BEEM model checking benchmarks [1] translated to the sequential BTOR format [2]. The original sources and authors of the benchmark models are listed in the online BEEM database [3]. In the subdirectory "btors", each file encodes an instance of a BEEM model and a reachability property. The files are named btors/..prop--.btor where is the name of the model, is a number identifying a specific parameterization of the model, and is a number identifying a reachability property. These names and numbers are as recorded in the BEEM database [3]. All 344 combinations of instances and reachability properties are included, with various encoding parameters (see below). LTL properties are left out, as are models for which BEEM does not define any reachability properties. See the file "expected-results.txt" for known model checking results for most of the instances and reachability properties. These results have been computed using an explicit-state model checker. The translation to BTOR attempts to be bit-accurate and cover all features of the models. The control locations are represented with 1-bit registers, the data variables with 8- and 16-bit registers, and intermediate values with 32-bit signed semantics. See [4] for more details. The encoding parameters and are described below. For each instance, two combinations are included. The combination func-interl might work better for verifying non-reachability, while back-serstep might yield witnesses to reachability faster. Interleaving transition relation ( = interl): In each execution step, a single action is executed. An action corresponds to a non-synchronizing transition in the BEEM system, or to a pair of transitions that synchronize on a channel. Serial exists-step transition relation ( = serstep): In each execution step of the circuit, one or more actions of the BEEM system are executed in a sequence. See [4]. Functional circuit encoding ( = func): The register outputs represent the current state xor the initial state, which is unique in BEEM. Thus, all-zero register values represent the initial state. The register inputs are functionally dependent on the register outputs and the primary inputs that select the current actions, according to the transition relation. The special register 'dve_invalid' remains 0, unless an action has been selected whose guard is false. The reachability property is conjuncted with 'dve_invalid = 0'. Backward circuit encoding ( = back): A valid execution is such that in the first step, the register inputs are set to values that satisfy the reachability property, and in all subsequent steps, the register inputs represent a predecessor state of the register outputs. The property to check is whether the register outputs can represent an initial state after one of more valid execution steps. The special register 'dve_initialized' is 1 everywhere except initially, and 'dve_valid' is 1 iff 'dve_initialized' is 1 and the execution is valid so far. References [1] R. Pelánek. BEEM: Benchmarks for Explicit Model Checkers. In Proc. SPIN 2007, LNCS vol. 4595, pp. 263--267, Springer 2007. [2] R. Brummayer, A. Biere, F. Lonsing. BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking. In Proc. 1st Intl. Workshop on Bit-Precise Reasoning (BPR'08), Princeton, New Jersey, USA, July 2008. [3] http://anna.fi.muni.cz/models/ 14th January 2010. [4] J. Dubrovin, T. Junttila, K. Heljanko. Exploiting Step Semantics for Efficient Bounded Model Checking of Asynchronous Systems. In Science of Computer Programming, Elsevier 2011. http://dx.doi.org/10.1016/j.scico.2011.07.005