FuseIC3 is a SAT-based algorithm for checking a set of models. It extends IC3 to minimize time spent in exploring the common state space between related models.
Rohit Dureja and Kristin Yvonne Rozier. “FuseIC3: An Algorithm for Checking Large Design Spaces.” In Formal Methods in Computer-Aided Design (FMCAD 2017), IEEE/ACM, Vienna, Austria, October 2-6, 2017.
For more details about FuseIC3, please visit: http://temporallogic.org/research/FMCAD17
- System Requirements
- MathSAT5 (mathsat.fbk.eu)
- C++11
- libgmp, libgmpxx
CMake is the default build tool. To install FuseIC3, download the unzip the repository. Run the following commands to build and install FuseIC3.
cd FuseIC3-master
mkdir build
cd build
cmake ..
make
Usage: ./FuseIC3 [options] folder
Algorithm options
-p priority-queue proof obligation management (default: false)
if not enabled, a stack-based approach is used
-f number enable model-set mode; set algorithm number between [1...4] (default: disabled)
folder path of folder containing .vmt files to check (required)
Miscellaneous
-v level set verbosity level (default: 0)
-w print witness (default: false)
-s seed seed value for random number generator
-h, --help display this message
Available model-set checking algorithms
(supplied as argument with -f options)
-----------------------------------------------------------------
| Number | Algorithm |
-----------------------------------------------------------------
| 1 | Incremental IC3 (FMCAD 2011) |
| 2 | Basic Check (re-use and check last invariant) |
| 3 | Basic Check + Drop Violating Clauses |
| 4 | Basic Check + Repair Violating Clauses |
-----------------------------------------------------------------
Example usage scenarios
./FuseIC3 folder runs simple IC3 algorithm on files in folder
./FuseIC3 -p folder runs simple IC3 algorithm using priority queues on files in folder
./FuseIC3 -f 3 folder runs model-sets checking algorithm number 3 on files in folder
./FuseIC3 -p -f 2 folder runs model-sets checking algorithm number 2 using priority queues on files in folder