A graph‐labeling approach for efficient cone‐of‐influence computation in model‐checking problems with multiple properties. (11th March 2015)

• Record Type: Journal Article
• Authors: Cabodi, Gianpiero; Camurati, Paolo; Quer, Stefano
• Is Part Of: Software, practice & experience. Volume 46:Number 4(2016)
• Page Start: 493
• Page End: 511
• Publication Date: 2015-03-11
• Subjects: model checking -- Boolean functions -- cone of influence -- graph labeling; Computer software -- Periodicals; Computer programming -- Periodicals; Computer programs -- Periodicals; 005.3
• DOI: 10.1002/spe.2321
• Languages: English
• ISSNs: 0038-0644

Abstract

Summary: 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. Copyright © 2015 John Wiley & Sons, Ltd.