Abstract
The existence of functional dependency among the state variables of a state transition system was identified as a common cause of inefficient BDD representation in formal verification. Eliminating such dependency from the system compacts the state space and may significantly reduce the verification cost. Despite the importance, how to detect functional dependency without or before knowing the reachable state set remains a challenge. This paper tackles this problem by unifying two closely related, but scattered, studies — detecting signal correspondence and exploiting functional dependency. The prior work on either subject turns out to be a special case of our formulation. Unlike previous approaches, we detect dependency directly from transition functions rather than from reached state sets. Thus, reachability analysis is not a necessity for exploiting dependency. In addition, our procedure can be integrated into reachability analysis as an on-the-fly reduction. Preliminary experiments demonstrate promising results of extracting functional dependency without reachability analysis. Dependencies that were underivable before, due to the limitation of reachability analysis on large transition systems, can now be computed efficiently. For the application to verification, reachability analysis is shown to have substantial reduction in both memory and time consumptions.
This work was supported in part by NSF grant CCR-0312676, California Micro program, and our industrial sponsors, Fujitsu, Intel and Synplicity.
Chapter PDF
References
Ashar, P., Gupta, A., Malik, S.: Using complete-1-distinguishability for FSM equivalence checking. In: Proc. ICCAD, pp. 346–353 (1996)
Berthet, C., Coudert, O., Madre, J.-C.: New ideas on symbolic manipulations of finite state machines. In: Proc. ICCD, pp. 224–227 (1990)
Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 372–389. Springer, Heidelberg (2000)
Brayton, R.K., et al.: VIS: a system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)
Brown, F.M.: Boolean Reasoning: The Logic of Boolean Equations. Dover Publications (2003)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers, 677–691 (August 1986)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
van Eijk, C.A.J., Jess, J.A.G.: Exploiting functional dependencies in finite state machine verification. In: Proc. European Design & Test Conf., pp. 9–14 (1996)
van Eijk, C.A.J.: Sequential equivalence checking based on structural similarities. IEEE Trans. Computer-Aided Design, 814–819 (July 2000)
Filkorn, T.: Symbolische methoden für die verifikation endlicher zustandssysteme. Ph.D. thesis. Institut für Informatik der Technischen Universität München (1992)
Hu, A.J., Dill, D.L.: Reducing BDD size by exploiting functional dependencies. In: Proc. DAC, pp. 266–271 (1993)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)
Lin, B., Newton, A.R.: Exact redundant state registers removal based on binary decision diagrams. In: Proc. Int’l Conf. VLSI, pp. 277–286 (1991)
Leiserson, C.E., Saxe, J.B.: Optimizing synchronous systems. J. VLSI Computer Syst. 1(1), 41–67 (1983)
Marczewski, E.: Independence in algebras of sets and Boolean algebra. Fundamenta Mathematicae 48, 135–145 (1960)
Quer, S., Cabodi, G., Camurati, P., Lavagno, L., Brayton, R.: Verification of similar FSMs by mixing incremental re-encoding, reachability analysis, and combinational check. Formal Methods in System Design 17, 107–134 (2000)
Sentovich, E., Toma, H., Berry, G.: Latch optimization in circuits generated from high-level descriptions. In: Proc. ICCAD, pp. 428–435 (1996)
Stoffel, D., Kunz, W.: Record & play: A structural fixed point iteration for sequential circuit verification. In: Proc. ICCAD, pp. 394–399 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jiang, JH.R., Brayton, R.K. (2004). Functional Dependency for Verification Reduction. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive