New in this release:
- Several improvements to IC3:
- CTGs (see FMCAD 2013 paper)
- Localization reduction engine
- Latest Minisat used for everything but IC3
- TVsim (ternary simulation engine)
- Phase abstraction
- Decoding for backward encoded models
- FCBMC (fair cycle BMC)
- GSH (BDD-based cycle detection)
- Several bugs fixes
- Improved efficiency for large designs
IImc 1.3 has been built on:
- Ubuntu 12.10, 13.04, and 13.10 with gcc
- Ubuntu 12.10 with clang
- Red Hat Enterprise 6.4 with gcc
- Current Cygwin on Windows 7, both 32- and 64-bits, with gcc
- OS X v10.7.5 and v10.8.5 with clang
The versions of gcc range from 4.4.7 to 4.8.2. Clang’s version is 3.0.
The tarball is available on the download page.
The IImc binary used for HWMCC’13 is now available on the download page. The binary is statically-linked so should run on a wide range of platforms. To run, do
This is a bug-fix release. Visit the download page to get the tarball.
A new version of IImc is available on the download page. The major addition to IImc 1.1 is the new CTL model checking engine from the CAV’12 paper: ”Incremental Inductive CTL Model Checking” by Z. Hassan, A. R. Bradley, and F. Somenzi.
Additions in Release 1.1:
- A new engine, IICTL, which is a new “IC3-like” model checking engine for CTL properties with fairness constraints
- A new BMC engine for fair-cycle detection
- Slightly improved performance for some of the model checking engines
- A few bug fixes
IImc 1.1 has been compiled with
clang++ 3.0, and has been tested on Ubuntu 12.04 and 12.10, Red Hat Enterprise 6.3, and Cygwin 1.7.
Welcome to IImc. The first release is ready on the download page!