Advertisement

Advancements in symbolic traversal techniques

  • Gianpiero Cabodi
  • Paolo Camurati
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)

Abstract

Symbolic state space traversal techniques are one of the most notable achievements in the fields of formal verification and of automated synthesis. Transition functions and transition relations are two alternative approaches. In terms of efficiency, transition functions have proven to be superior, although the transition relation is much more expressive. This paper brings the transition relation back to a new life, profiting from recent advancements in the fields of boolean function representation, simplification, and image computation represented by BDDs and by the generalized cofactor operator. A theoretical result allows us to considerably simplify both the process of building the transition relation and of traversing the state space. Experimental results show that performances similar to those of the transition function are obtained.

Keywords

Transition Function Boolean Function Transition Relation Garbage Collection Formal Verification 
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

  1. 1.
    Brglez, F. Bryan, D., Koźmiński, K.: Combinatorial Profiles of Sequential Benchmark Circuits. ISCAS'89: IEEE Int'l Symposium on Circuits and Systems, Portland, OR (USA), May 1989, pp. 1929–1934Google Scholar
  2. 2.
    Burch, J.R., Clarke, E.M., Long, D.E.: Representing Circuits More Efficiently in Symbolic Model Checking. DAC'91: 28th ACM/IEEE Design Automation Conference, San Francisco, CA (USA), June 1991, pp. 403–407Google Scholar
  3. 3.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. LICS'90: 5th Annual IEEE Symposium on Logic in Computer Science, June 1990, pp. 428–439Google Scholar
  4. 4.
    Bochmann, D., Dreisig, F., Steinbach, B.: A new Decomposition Method for Multilevel Circuit Design. EDAC'91: IEEE European Conference on Design Automation, Amsterdam (The Netherlands), February 1991, pp. 374–377Google Scholar
  5. 5.
    Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient Implementation of a BDD Package. DAC'90: 27th ACM/IEEE Design Automation Conference, Orlando, FL (USA), June 1990, pp. 40–45Google Scholar
  6. 6.
    Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computer, Vol. C-35, No. 8, August 1986, pp. 677–691Google Scholar
  7. 7.
    Coudert, O., Berthet, C., Madre, J.C.: Verification of Sequential Machines Based on Symbolic Execution. “Automatic verification methods for finite state systems,”, J. Sifakis editor, Lecture Notes in Computer Science 407, Springer Verlag, Berlin (Germany), 1989, pp. 365–373Google Scholar
  8. 8.
    Coudert, O., Berthet, C., Madre, J.C.: Verification of Sequential Machines Using Boolean Function Vectors. IFIP Int'l Workshop on “Applied Formal Methods for Correct VLSI Design”, Leuven (Belgium), November 1989, Vol. 1, pp. 111–128Google Scholar
  9. 9.
    Cabodi, G.P., Camurati, P., Corno, F., Gai, S., Prinetto, P., Sonza Reorda, M.: A new Model for Improving Symbolic Product Machine Traversal. DAC-29: 29th ACM/IEEE Desing Automation Conference, Anaheim, CA (USA), June 1992, pp. 614–619Google Scholar
  10. 10.
    Camurati, P., Corno, F., Prinetto, P.: Exploiting symbolic traversal techniques for efficient Process Algebra Manipulation. CHDL'93: IFIP Conference on Hardware Description Languages and their Applications, Ottawa (Canada), April 1993Google Scholar
  11. 11.
    Cho, H., Hachtel, G., Jeong, S.W., Plessier, B., Schwarz, E., Somenzi, F.: ATPG Aspects of FSM Verification. ICCAD-90: IEEE Int'l Conference on Computer Aided Design, Santa Clara, CA (USA), November 1990, pp. 134–137Google Scholar
  12. 12.
    Coudert, O., Madre, J.C.: A Unified Framework for the Formal Verification of Sequential Circuits. ICCAD-90: IEEE Int'l Conf. on Computer Aided Design, Santa Clara, CA (USA), November 1990, pp. 126–129Google Scholar
  13. 13.
    Coudert, O., Madre, J.C.: Symbolic Computation of the Valid States of the Sequential Machine: Algorithms and Discussion. 1991 Int'l Workshop on Formal Methods in VLSI Design, Miami, FL (USA), January 1991Google Scholar
  14. 14.
    Enders, R., Filkorn, T., Taubner, D.: Generating BDDs for Symbolic Model Checking in CCS. CAV'91: Computer-Aided Verification Workshop, Aalborg (Denmark), July 1991, K.G. Larsen, A. Skou Editors, Lecture Notes in Computer Science 575, Springer Verlag, Berlin (Germany), pp. 203–213Google Scholar
  15. 15.
    Kohavi, Z.: Switching and Finite Automata Theory, second edition, Computer Science Series, Mc Graw Hill, New York, NYGoogle Scholar
  16. 16.
    Touati, H., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit Enumeration of Finite State Machines Using BDDs. ICCAD-90: IEEE International Conference on Computer Aided Design, Santa Clara, CA (USA), November 1990, pp. 130–133Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Gianpiero Cabodi
    • 1
  • Paolo Camurati
    • 1
  1. 1.Dipartimento di Automatica e InformaticaPolitecnico di TorinoTurinItaly

Personalised recommendations