Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking

IC3 is one of the most successful algorithms for hardware model checking. Since its invention in 2010, several variants of the original algorithm have been published, proposing optimizations and/or alternative procedures for the many different steps of the algorithm. In this paper, we present a thorough empirical comparison of a large set of optimizations and procedures for the steps of IC3, considering "high-level" variants/extensions to the basic algorithm, as well as "low-level" optimizations/configuration settings. We implemented each of them in the same tool, optimizing the implementations to the best of our knowledge. This enabled for a flexible experimentation in a controlled environment, and to gain new insights about their most important differences and commonalities, as well as about their performance characteristics. We conducted the experiments using as benchmarks the problems used in the last four editions of the hardware model checking competition. The analysis helped us to identify several settings leading to significant improvements wrt. a basic implementation of IC3.