A graph-labeling approach for efficient cone-of-influence computation in model-checking problems with multiple properties

In order to make model checking applicable to realistic problems, simplification techniques are essential. Models may be simplified eliminating the variables that do not appear in the cone-of-influence (COI) of the properties under verification. Efficient COI computation is thus required. Algorithms based on depth-first visits may become cumbersome when they must be applied several times; for instance, when multiple properties must be verified on the same model. An alternative is to resort to graph-labeling methods, trading-off time for memory. Modeling the problem in terms of graphs, this paper develops a technique based on bitmaps that keeps the amount of memory needed within acceptable limits. The paper also describes a portfolio of optimizations of the original algorithm that allow even more reductions in memory usage. Experimental results show that the basic algorithm and its optimized versions perform very well on standard benchmark circuits used in the model-checking community.