Abstract
Model checking is the process of verifying whether a model of a concurrent system satisfies a specified temporal property. Symbolic algorithms based on Binary Decision Diagrams (BDDs) have significantly increased the size of the models that can be verified. The main problem in symbolic model checking is the image computation problem, i.e., efficiently computing the successors or predecessors of a set of states. This paper is an in-depth study of the image computation problem. We analyze and evaluate several new heuristics, metrics, and algorithms for this problem. The algorithms use combinatorial optimization techniques such as hill climbing, simulated annealing, and ordering by recursive partitioning to obtain better results than was previously the case. Theoretical analysis and systematic experimentation are used to evaluate the algorithms.
This research is sponsored by the Semiconductor Research Corporation (SRC), the Gigascale Research Center (GSRC), the National Science Foundation (NSF) under Grant No. CCR-9505472, and the Max Kade Foundation. One of the authors is also supported by Austrian Science Fund Project N Z29-INF. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily re.ect the views of GSRC, NSF, or the United States Government.
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
J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in Symbolic Model Checking. In 28th ACM/IEEE Design Automation Conference, 1991.
J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic Model Checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proceedings of the International Conference on Very Large Scale Int egration, Edinburgh, Scotland, August 1991.
C. J. P. B’elisle. Convergence theorems for a class of simulated annealing algorithms. Journal of Applied Probability, 29:885–892, 1992.
T. N. Bui and C. Jones. Finding good approximate vertex and edge partitions is NP-hard. Information Processing Letters, 42:153–159, 1992.
A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Proceedings of International Conference on Computer-Aided Verification (CAV’99), number 1633 in Lecture Notes in Computer Science, pages 495–499. Springer, July 1999.
E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.
C.M. Fiduccia and R.M. Mattheyses. A linear time heuristic for improving network partitions. In 19th ACM/IEEE Design Automation Conference, pages 175–181, 1982.
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), volume 818 of LNCS, pages 299–310, Stanford, CA, USA, 1994. Springer-Verlag.
Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., 1979.
B. Hajek. A tutorial survey of theory and applications of simulated annealing. In Proc. 24th IEEE Conf. Decision and Control, pages 755–760, 1985.
S. Kirkpatrick, C. D. Gelatt Jr., and M. P. Vecchi. Optimization by simulated annealing. Science, 220:671–679, 1983.
Brian Kernighan and S. Lin. An efficient heuristic procedure for partitioning graphs. The Bell System Technical Journal, pages 291–307, February 1970.
In-Ho Moon, James H. Kukula, Kavita Ravi, and Fabio Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the 37th Design Automation Conference (DAC’00), pages 26–28, Los Angeles, June 2000.
N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, and E. Teller. Equation of state calculations by fast computing machines. Journal of Chemical Phyics, 21(6):1087–1092, 1953.
In-Ho Moon and Fabio Somenzi. Border-block triangular form and conjunction schedule in image computation. In Warren A. Hunt Jr. and Steven D. Johnson, editors, Proceedings of the Formal Methods in Computer Aided Design (FMCAD’00), volume 1954 of LNCS, pages 73–90, November 2000.
R.K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R.K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In IEEE/ACM International Workshop on Logic Synthesis, Lake Tahoe, 1995. IEEE/ACM.
H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDDs. In Proceedings of the IEEE international Conference on Computer Aided Design (ICCAD), pages 130–133, November 1990.
Bwolen Yang. Optimizing Model Checking Based on BDD Characterization. PhD thesis, Carnegie Mellon University, Computer Science Department, May 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chauhan, P., Clarke, E., Jha, S., Kukula, J., Veith, H., Wang, D. (2001). Using Combinatorial Optimization Methods for Quantification Scheduling. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_24
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive