Abstract
In symbolic model checking, image computation is the process of computing the successors of a set of states. Containing the cost of image computation depends critically on controlling the number of variables that appear in the functions being manipulated; this in turn depends on the order in which the basic operations of image computation-conjunctions and quantifications-are performed. In this paper we propose an approach to this ordering problem-the conjunction scheduling problem-that is especially suited to the case in which the transition relation is specified as the composition of many small relations. (This is the norm in hardware verification.) Our fine-grain approach leads to the formulation of conjunction scheduling in terms of minimum max-cut linear arrangement, an NP-complete problem for which efficient heuristics have been developed. The cut whose width is minimized is related to the number of variables active during image computation.We also propose a clustering technique that is geared toward the minimization of the max-cut, and pruning techniques for the transition relation that benefit especially from the fine-grain approach.
Work performed in part while the author was at Cadence Berkeley Labs.
Work supported in part by SRC contract 2001-TJ-920 and NSF grant CCR-99-71195.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Fifth International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’99), pages 193–207, Amsterdam, The Netherlands, March 1999.
R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eighth Conference on Computer Aided Verification (CAV’96), pages 428–432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.
R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design, 13(4):401–424, April 1994.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, pages 428–439, June 1990.
G. Cabodi, P. Camurati, and S. Quer. Improved reachability analysis of large finite state machines. In Proceedings of the International Conference on Computer-Aided Design, pages 354–360, Santa Clara, CA, November 1996.
A. E. Caldwell, A. B. Kahng, and I. Markov. Optimal partitioners and end-case placers for standard-cell layout. IEEE Transactions on Computer-Aided Design, 19(11):1304–1314, November 2000.
P. P. Chauhan, E. M. Clarke, S. Jha, J. Kukula, T. Shiple, H. Veith, and D. Wang. Nonlinear quantification scheduling in image computation. In Proceedings of the International Conference on Computer-Aided Design, pages 293–298, San Jose, CA, November 2001.
O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines based on symbolic execution. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, pages 365–373. Springer-Verlag, 1989. LNCS 407.
O. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 126–129, November 1990.
M. R. Garey, D. S. Johnson, and L. Stockmeyer. Some simplified NP-complete graph problems. Theoretical Computer Science, pages 237–267, 1987.
D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation partitions. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV’94), pages 299–310, Berlin, 1994. Springer-Verlag. LNCS 818.
A. Gupta, Z. Yang, L. Zhang, and S. Malik. Partition-based decision heuristics for image computation using SAT and BDDs. In Proceedings of the International Conference on Computer-Aided Design, pages 286–292, San Jose, CA, November 2001.
R. Hojati, S. C. Krishnan, and R. K. Brayton. Early quantification and partitioned transition relations. In Proceedings of the International Conference on Computer Design, pages 12–19, Austin, TX, October 1996.
I-H. Moon, G. D. Hachtel, and F. Somenzi. Border-block triangular form and conjunction schedule in image computation. In W.A. Hunt, Jr. and S. D. Johnson, editors,Formal Methods in Computer Aided Design, pages 73–90. Springer-Verlag, November 2000. LNCS 1954.
I.-H. Moon, J. H. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23–28, Los Angeles, CA, June 2000.
R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. Presented at IWLS95, Lake Tahoe, CA., May 1995.
C. H. West and P. Zafiropulo. Automated validation of a communications protocol: The CCITT X.21 recommendation. IBM Journal of Research and Development, 22:60–71, 1978.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jin, H., Kuehlmann, A., Somenzi, F. (2002). Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_22
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive