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
IImc can be built with or without zchaff. For details, please refer to LICENSE.zchaff.
The IImc home page and forum are on:
http://iimc.colorado.eduThe most recent version of the GNU tools:
http://www.gnu.orgThe most recent version of the boost libraries:
http://www.boost.orgDownload the most recent version of IImc from:
into a convenient directory, (e.g. /tmp).
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
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.
Build IImc by running make:
$ make
This builds an executable "iimc" in the current directory. Parallel build trees are also supported.
Verify that IImc works by running it on some of the examples included in the distribution:
$ make check
To build IImc on Apple's OS X you need to have the boost libraries installed. This is what worked for us:
Download from www.boost.org a recent version (e.g., 1.55.0)
Untar
Run ./boostrap.sh
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):
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.)
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:
Configure IImc using
./configure CC=clang CXX=clang++ CXXFLAGS="-stdlib=libc++ -g -O3" CPPFLAGS=-Dthread_local="__thread" YACC="/usr/local/bin/bison -y"
make
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
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
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
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
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
--
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.
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.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.
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
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
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
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.)
[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.