mgudemann/iimc
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
Repository files navigation
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.