This is release 2.0 of IImc, an Incremental Inductive model checker. IImc
features novel formal engines such as IC3[1,2], FAIR[3], and IICTL[4].

IImc is developed by MC@CU, the model checking group at the University of
Colorado at Boulder. IImc's authors are Aaron Bradley, Arlen Cox,
Michael Dooley, Zyad Hassan, Fabio Somenzi, and Yan Zhang.

This file describes how to build IImc and then provides a quick
introduction to its use.

-------------------------------------------------------------------------------
To build IImc, you will need

  * GNU C++ (g++) version 4.8.2 or higher
  * Alternatively, IImc can be compiled with clang++ 3.4 or higher
  * GNU's make utility
  * The boost library (at the very least, the "Boost Program Options",
    "Boost Random", and "Boost Regex" libraries)
  * GNU Flex
  * GNU Bison version 2.4.1 or higher
  * zlib (including the header file zlib.h)

IImc can be built with or without zchaff.  For details, please refer to
LICENSE.zchaff.

-------------------------------------------------------------------------------
* Useful Addresses

The IImc home page and forum are on:

    http://iimc.colorado.edu

The most recent version of the GNU tools:

    http://www.gnu.org

The most recent version of the boost libraries:

    http://www.boost.org

-------------------------------------------------------------------------------
* Building IImc

1. Download the most recent version of IImc from:

    http://iimc.colorado.edu

   into a convenient directory, (e.g. /tmp).

2. Move to where you would like to build IImc and unpack the distribution:

    $ cd /home/iimc                           # for example
    $ tar xvzf /tmp/iimc-2.0.tar.gz

3. Move into the iimc-2.0 directory and run configure, which will determine
   some system-specific parameters and create the Makefile

    $ cd iimc-2.0
    $ ./configure

   You may want to pass --enable-silent-rules to configure.

4. Build IImc by running make:

    $ make

   This builds an executable "iimc" in the current directory.  Parallel build
   trees are also supported.

5. Verify that IImc works by running it on some of the examples included
   in the distribution:

    $ make check

-------------------------------------------------------------------------------
* Building IImc on OS X

To build IImc on Apple's OS X you need to have the boost libraries
installed.  This is what worked for us:

1. Download from www.boost.org a recent version (e.g., 1.55.0)

2. Untar

3. Run ./boostrap.sh

4. Install using 
     sudo ./b2 toolset=clang cxxflags="-stdlib=libc++" linkflags="-stdlib=libc++" install

You may need to add "address-model=64" to the b2 invocation.

You also need to have a recent version of bison (IImc requires 3.0.2
or higher):

1. Download from www.gnu.org/software/bison a recent version. (E.g.,
   3.0.2.  Xcode currently ships bison 2.3, which is too old.)

2. Untar, configure, make, make install.

By default, the new bison will be installed in /usr/local and will not
overwrite what is already on your system.  You may also get bison via
macports, in which case it should be installed in /opt/local.

Installation of IImc now takes the following steps:

1. Configure IImc using 

  ./configure CC=clang CXX=clang++ CXXFLAGS="-stdlib=libc++ -g -O3" CPPFLAGS=-Dthread_local="__thread" YACC="/usr/local/bin/bison -y"

2. make

3. make check

-------------------------------------------------------------------------------
* Quick-start guide for using IImc

  The input formats accepted by IImc are the AIGER 1.0 and AIGER 1.9
  formats[5]. The easiest way to launch IImc is through doing

  iimc <aiger-file>

  or if it is desired to model check a CTL property, the property should be
  specified in a separate file (see next section for the syntax of CTL files),
  and IImc should be invoked through

  iimc --ctl <ctl-file> <aiger-file>

  If the AIGER file contains multiple properties as allowed by the AIGER 1.9
  format, the property can be selected using the --pi option, i.e.,

  iimc --pi 3 <aiger-file> 

  will select the property with index 3 in the AIGER file. Similarly, for a CTL
  file with multiple properties, the --pi option can be used to select the
  desired property.

  The output from IImc follows the standard for the hardware model checking
  competition[6], in which a "0" output indicates that the property holds, a
  "1" output indicates that the property fails, and a "2" output indicates that
  the result is unknown.

  IImc normally runs in the silent mode in which nothing is printed out except
  for the final result as indicated in the previous paragraph and the so-called
  u-lines that report lower bounds on the length of a counterexample, if indeed
  there exists one. To turn up the verbosity, the -v option can be used, where
  -v 4 prints lots of debugging information, and -v 0 is the silent mode.

-------------------------------------------------------------------------------
* Specifying CTL properties for IImc

  CTL properties need to be provided in a separate file, which is then passed
  to IImc using the --ctl <ctl-file> option.

  A CTL file can contain multiple CTL properties. A line that begins with a '#'
  is a comment. The allowed CTL operators are EX, EF, EG, EU, ER, EW, and their
  universal counterparts. The Boolean connectives ~, &, |, ^, ==, -> denote
  negation, conjunction, disjunction, XOR, equivalence, and implication
  respectively. ! can also be used for negation.

  Any id used, must be defined in the AIGER file's symbol table. An id can
  refer to a latch or an output.

  Example 1: AG(~error)
  specifies that the output named "error" must always stay at 0. The
  parentheses are optional.

  Example 2: AG(req -> AF ack)
  specifies that whenever a request occurs, an acknowledgement eventually
  follows.

  Example 3: E ~Heat U Close
  specifies that there exists a path in which "Heat" is false until "Close"
  becomes true.

  For more examples, check the .ctl files in examples/ctl/ .

-------------------------------------------------------------------------------
* More detailed guide for using IImc

  IImc includes a number of formal engines as well as a number of combinational
  and sequential circuit simplification engines. Each of those engines is
  called an action or a tactic. Applying a certain tactic can be done by
  supplying the "-t" option followed by the tactic's name. Multiple tactics can
  be applied in sequence by preceding each of the tactic's names by the "-t"
  option and writing them in the desired order , e.g., -t tactic1 -t tactic2.
  
  This is the list of formal engines currently available in IImc with the
  corresponding tactic name:

  a. BDD Backward Reachability:  bdd_bw_reach
  b. BDD Forward Reachability:   bdd_fw_reach
  c. BMC:                        bmc
  d. BMC for fair cycles:        fcbmc
  e. Fair[3]:                    fair
  f. FSIS[7]:                    fsis
  g. BDD-based cycle detection:  gsh
  h. IC3:                        ic3
  i. Reverse IC3:                ic3r
  j. Localization reduction IC3: ic3lr
  k. IICTL:                      iictl
  l. k-Liveness for fair cycles: klive

  The list of circuit simplification engines currently available in IImc with
  the corresponding tactic name follows.

  a. BDD Sweeping:                                        bddsweep
  b. Cut Sweeping:                                        cutsweep
  c. SAT Sweeping:                                        satsweep
  c. Cone-of-Influence Reduction:                         coi
  d. Latch Sequential Equivalence (Latch Correspondence): se
  e. Latch Stuck-at-Value Detection:                      stuck
  f. Phase Abstraction:                                   phase
  g. Ternary simulation:                                  tvsim
  h. Abstract interpretation:                             absint
  i. Decoding:                                            decode
  j. Slicing:                                             slice
  k. Sequential Reduction (applies coi, stuck, and se):   sr
  l. Preprocessing (applies coi, absint, tvsim, satsweep,
                    bddsweep, se, and stuck):             pp

  Invoking IImc without any tactics invokes the default "standard"
  tactic, which sets suitable options, and then runs preprocessing
  followed by the appropriate combination of formal engines depending
  on the property type (IICTL for a CTL property, and a sequence of
  engines for a safety or justice property).  The "standard" tactic
  prints a counterexample for a failing safety proprty and also prints
  u-lines, which give lower bounds on the length of a counterexample
  if one exists.

  If you want to choose a different combination of preprocessing
  tactics, but still apply the default combination of proof engines,
  choose tactic "check".

  For each tactic, there are usually multiple options available (e.g.,
  timeout, parameters, etc.). Supplying options can be done using

    --<option-name> <option-value-if-available>, 

  which can be written anywhere in the command-line arguments. For
  example:

    -t ic3 --ic3_timeout 10

  is the same as

    --ic3_timeout 10 -t ic3

  To view a list of available options, do

    ./iimc -h

  or use the long form
   
    ./iimc --help

  IImc 2.0 multi-threaded execution is based on a portfolio approach.
  Combinations of proof engines are supported by special tactics:
  fork, join, begin, end.  While these tactics are exposed by the
  interface, only a few of the syntactically meaningful combinations
  are supported and they are not meant for general use.

-------------------------------------------------------------------------------
* Example Sessions

1. To run IImc's IC3 engine on the gcd16flat.aig example, use the following:

    ./iimc -t ic3 examples/aig/gcd16flat.aig

   which would produce:

    1

   indicating that the property is SAT. To control verbosity, use -v
   <0-4> with 0 being the default and 4 indicating maximum verbosity.

2. To perform cone-of-influence reduction and follow that by 10 seconds of
   BMC and 5 seconds of IC3 on the smult8aflat example, and run that with
   verbosity level 1, do:

    ./iimc -v1 -t sr -t bmc --bmc_timeout 10 -t ic3 --ic3_timeout 5 examples/aig/smult8aflat.aig

   which produces:

   Input File is examples/aig/smult8aflat.aig
   ExprAttachment: building from file
   SeqAttachment: building
   COIAttachment: building
   COI: Initial # latches = 21
   COI: Final # latches = 5
   AIGAttachment: Building AIG for model examples/aig/smult8aflat.aig
   StuckAt: Found 0 stuck-at latches
   SequentialEquivalence: Initial # latches = 5
   SequentialEquivalence: Final # latches = 5
   Sequential equivalence completed in 0 s
   COI: Initial # latches = 5
   COI: Final # latches = 5
   Building proof attachment for model examples/aig/smult8aflat.aig
   RchAttachment: building
   CNFAttachment: building CNF using Tseitin translation
   BMC: Checking up to 8191
   Conclusion found by BMC.
   1

   where IC3 did not get to run because BMC already found the property
   to be SAT.

3. To run cut sweeping followed by SAT sweeping followed by BDD forward
   reachability with verbosity level of 2 on the sfeistelp1 example, do

    ./iimc -v2 -t cutsweep -t satsweep -t bdd_fw_reach examples/aig/sfeistelp1.aig
 
   which produces something like:

   Input File is examples/aig/sfeistelp1.aig
   # ./optimized/iimc -v2 -t cutsweep -t satsweep -t bdd_fw_reach
   # examples/aig/sfeistelp1.aig
   ExprAttachment: building from file
   AIGAttachment: Building AIG for model main
   CombAttachment: building
   Cut Sweeping: timeout disabled
   Cut Sweeping: before cut sweeping, AIG has 7763 nodes (Use -v4 to dump AIG)
   Cut Sweeping: in process (s=250, N=1)...
   Cut Sweeping: found 1120 merges
   Cut Sweeping: generated 13116 cuts
   Cut Sweeping: used 6241 cuts in enumeration
   Cut Sweeping: 0.03s spent in sweeping
   Cut Sweeping: new AIG has 5186 nodes
   SAT Sweeping: Number of AIG nodes = 5186
   SAT Sweeping: Running with a timeout of 10 seconds + 0 seconds of relayed time
   SAT Sweeping: Merged a total of 31 nodes.
   SAT Sweeping: New AIG has 5079 nodes
   SAT Sweeping: 0.07s spent in sweeping
   SAT Sweeping: Percentage Reduction = 2.06%
   SAT Sweeping: Number of SAT checks = 70 (39 SAT/31 UNSAT/0 Timed Out)
   SAT Sweeping: Number of ignored candidate equivalences due to SAT solver timeout = 0
   ExprAttachment: building from AIG
   CombAttachment: building
   Building BDDs for model main
   Static BDD variable ordering method: interleaving
   4803 BDD nodes
   0 auxiliary variables
   Computing transition relation for model main
   number of variables = 654
   BDD reordering with sifting: from 5229 to ... 4948 nodes in 0.13 sec
   Output function: 1047 nodes 1 leaves 4.97323e+86 minterms
   BDD reordering with sifting: from 9897 to ... 7979 nodes in 0.4 sec
   BDD reordering with sifting: from 15959 to ... 8344 nodes in 0.43 sec
   BDD reordering with sifting: from 16689 to ... 8661 nodes in 0.44 sec
   BDD reordering with sifting: from 17323 to ... 8703 nodes in 0.46 sec
   BDD reordering with sifting: from 17407 to ... 9168 nodes in 0.48 sec
   BDD reordering with sifting: from 18337 to ... 9345 nodes in 0.48 sec
   BDD reordering with sifting: from 18691 to ... 12056 nodes in 0.77 sec
   BDD reordering with sifting: from 24113 to ... 11733 nodes in 0.62 sec
   BDD reordering with sifting: from 23467 to ... 13065 nodes in 0.75 sec
   BDD reordering with sifting: from 26131 to ... 13528 nodes in 0.77 sec
   BDD reordering with sifting: from 27057 to ... 14982 nodes in 0.89 sec
   Number of clusters/nodes = 12/6537
   Initial condition: 294 nodes 1 leaves 1 minterms
   Building proof attachment for model main
   RchAttachment: building
   Forward Reachability analysis
   frontier 0: 294 nodes 1 leaves 1 minterms
   frontier 1: 459 nodes 1 leaves 5.53402e+19 minterms
   frontier 2: 966 nodes 1 leaves 3.40282e+38 minterms
   frontier 3: 1146 nodes 1 leaves 1.25542e+58 minterms
   BDD reordering with sifting: from 29962 to ... 25524 nodes in 1.94 sec
   frontier 4: 2556 nodes 1 leaves 1.25542e+58 minterms
   frontier 5: 727 nodes 1 leaves 1.25542e+58 minterms
   frontier 6: 2760 nodes 1 leaves 1.25542e+58 minterms
   frontier 7: 725 nodes 1 leaves 1.25542e+58 minterms
   frontier 8: 2758 nodes 1 leaves 1.25542e+58 minterms
   BDD reordering with sifting: from 51048 to ... 24375 nodes in 1.11 sec
   frontier 9: 1546 nodes 1 leaves 1.25542e+58 minterms
   frontier 10: 3327 nodes 1 leaves 1.25542e+58 minterms
   BDD reordering with sifting: from 48740 to ... 36784 nodes in 3.01 sec
   frontier 11: 6068 nodes 1 leaves 2.51084e+58 minterms
   BDD reordering with sifting: from 73545 to ... 59540 nodes in 3.39 sec
   frontier 12: 4242 nodes 1 leaves 2.31584e+77 minterms
   frontier 13: 7530 nodes 1 leaves 2.31584e+77 minterms
   Failure for output: 4486 nodes 1 leaves 4.97323e+86 minterms
   1

4. To run IICTL preceded by sequential reduction on the first CTL property of
   model rrobin with the output from all engines suppressed except for that
   from IICTL, do,

   ./iimc -v0 --iictl_verbosity 3 -t sr -t iictl --ctl examples/ctl/rrobin.ctl
   examples/ctl/rrobin.aig --pi 0

   for which the following output is produced:

   let d1114112 = & req0 req1 in
   let d1179648 = & !ack0 d1114112 in
   let d1245184 = & !ack1 d1179648 in
   let d1638400 = X !ack0 in
   let d1703936 = & d1245184 !d1638400 in
   let d1769472 = & d1245184 d1638400 in
   let d1835008 = U !d1703936 d1769472 in
   !d1835008
   
   IICTL: starting
   Checking LB initiation:
   Some initial states are not in LB
   Checking UB initiation:
   All initial states are in UB
   ========== Not ==========
   ========== EU ==========
   EU UB: SAT 0 seconds
   !ack0!ack1req0req1!robin
   00110
   EU LB: UNSAT 0 seconds
   ========== And ==========
   ========== EX ==========
   EX UB: UNSAT
   Checking LB initiation:
   Checking UB initiation:
   Checking LB initiation:
   Some initial states are not in LB
   Checking UB initiation:
   All initial states are in UB
   ========== Not ==========
   ========== EU ==========
   EU UB: UNSAT 0 seconds
   Checking LB initiation:
   0

5. Multi-threaded execution may be required by not specifying any
   tactic, as in:

    ./iimc examples/aig/gcd16flat.aig

   which produces the following output:

   u1
   1
   c witness
   b0
   00000000000000000000000000000000000000000000000000
   1xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
   000000000000000010000000000000001
   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
   .
   c end witness

   which shows the counteexample in AIGER format as well a u-line.
   Specify a higher verbosity level to observe more details of the
   execution.  (For instance, to know how many threads were spawned
   and which engine found the conclusion.)

-------------------------------------------------------------------------------

* References:

[1] A. R. Bradley, "k-step relative inductive generalization.", Technical
    Report, CU Boulder, Mar. 2010. http://arxiv.org/abs/1003.3649.

[2] A. R. Bradley, "SAT-based model checking without unrolling.", In
    Verification, Model Checking, and Abstract Interpretation (VMCAI'11), pages
    70-87, Austin, TX, Jan. 2011. LNCS 6538.

[3] A. R. Bradley, F. Somenzi, Z. Hassan, and Y. Zhang, "An incremental
    approach to model checking progress properties.", In Formal Methods in
    Computer Aided Design (FMCAD'11), pages 144-153, Austin, TX, Nov. 2011.

[4] Z. Hassan, A. R. Bradley, and F. Somenzi, "Incremental Inductive CTL Model
    Checking.", in Computer-Aided Verification (CAV'12), pages 532-547,
    Berkeley, CA, Jul. 2012.

[5] The AIGER format, http://fmv.jku.at/aiger/

[6] The hardware model checking competition, http://fmv.jku.at/hwmcc/

[7] A. R. Bradley and Z. Manna, "Checking safety by inductive generalization of
    counterexamples to induction.", In Formal Methods in Computer Aided Design
    (FMCAD'07), pages 173-180, Austin, TX, Nov. 2007.

[8] Z. Hassan, A. R. Bradley, and F. Somenzi, "Better Generalization in IC3."
    In Formal Methods in Computer Aided Design (FMCAD'13), pages 157-164, 
    Potland, OR, Oct. 2013.