Abstract
BDDs allow succinct symbolic representation of digital circuits. Symmetry reduction factors out redundancy inherent in the regular organization of many systems. Both are successful techniques for combating state space explosion. It would be desirable to combine them into symbolic symmetry reduction. Unfortunately, the straight-forward approach to symmetry reduction requires the orbit relation, whose symbolic representation as a BDD is in general of exponential size. We investigate the use of generic representatives as a means of overcoming this problem for fully symmetric systems: instead of first representing the system as a BDD and then applying symmetry reduction, we translate the given program text into a symmetry-reduced version. The result can then be encoded using a BDD. We demonstrate that this method is superior not only to the traditional orbit-relation based symmetry reduction, but also to the approach using multiple representatives.
This work was supported in part by NSF grants CCR-009-8141 and CCR-020-5483, and SRC contract 2002-TJ-1026.
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
Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers 35(8) (1986)
Barner, S., Grumberg, O.: Combining Symmetry Reduction and Under- Approximation for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 93. Springer, Heidelberg (2002)
Clarke, E.M., Allen Emerson, E.: The Design and Synthesis of Synchronization Skeletons Using Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, Springer, Heidelberg (1982)
Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting Symmetr. In: Temporal Logic Model Checking. Formal Methods in System Design 9 (1996)
Clarke, E.M., Allen Emerson, E., Jha, S., Prasad Sistla, A.: Symmetry Reductions in Model Checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)
Dill, D.L., Drexler, A.J., Hu, A.J., HanYang, C.: ProtocolVerification as a Hardware Design Aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors (1992)
Allen Emerson, E., Jha, S., Peled, D.: Combining Partial Order and Symmetry Reductions. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, Springer, Heidelberg (1997)
Allen Emerson, E., Srinivasan, J.: A Decidable Temporal Logic to Reason About Many Processes. Principles of Distributed Computing (1990)
Allen Emerson, E., Prasad Sistla, A.: Symmetry and Model Checking. Formal Methods in System Design 9 (1996) ISSN 0925-9856
Allen Emerson, E., Trefler, R.J.: From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999)
Norris Ip, C., Dill, D.L.: Better Verification Through Symmetry. Formal Methods in System Design 9(1/2) (1996)
Lin, B., Richard Newton, A.: Efficient symbolic manipulation of equivalence relations and classes. In: International Workshop on Formal Methods in VLSI Design (1991)
Mellor-Crummey, J.M., Scott, M.L.: Algorithms for Scalable Synchronization on Shared-memory Multiprocessors. ACM Transactions on Computer Systems 9 (1991)
McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, Dordrecht (1993)
Pixley, C.: Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, Springer, Heidelberg (1991)
Pong, F., Dubois, M.: A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems 6(8) (1995)
Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1,∞)-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 107. Springer, Heidelberg (2002)
Somenzi, F.: The CU Decision Diagram Package, release 2.3.1, http://vlsi.colorado.edu/~fabio/CUDD/
Wolper, P.: Expressing Interesting Properties of Programs. In: 13th Annual ACM Symposium on Principles of Programming Languages, POPL (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Wahl, T. (2003). On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive