Advertisement

Hints to Accelerate Symbolic Traversal

  • Kavita Ravi
  • Fabio Somenzi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)

Abstract

Symbolic model checking is an increasingly popular debugging tool based on Binary Decision Diagrams (BDDs). The size of the diagrams, however, often prevents its application to large designs. The lack of flexibility of the conventional breadth-first approach to state search is often responsible for the excessive growth of the BDDs. In this paper we show that the use of hints to guide the exploration of the state space may result in orders-of-magnitude reductions in time and space requirements. We apply hints to invariant checking. The hints address the problems posed by difficult image computations, and are effective in both proving and refuting invariants. We show that good hints can often be found with the help of simple heuristics by someone who understands the circuit well enough to devise simulation stimuli or verification properties for it. We present an algorithm for guided traversal and discuss its efficient implementation.

Keywords

Image Computation Model Check Transition Relation Parse Tree Reachable State 
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.
    M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    A. Aziz, J. Kukula, and T. Shiple. Hybrid verification using saturated simulation. In Proc. of the Design Automation Conference, pages 615–618, San Francisco, CA,June 1998.Google Scholar
  3. 3.
    I. Beer, S. Ben-David, and A. Landver. On-the-fly model checking of RCTL formulas. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV’98), pages 184–194. Springer-Verlag, Berlin, 1998. LNCS 1427.CrossRefGoogle Scholar
  4. 4.
    R. K. Brayton et al. VIS. In Formal Methods in Computer Aided Design, pages 248–256. Springer-Verlag, Berlin, November 1996. LNCS 1166.CrossRefGoogle Scholar
  5. 5.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.CrossRefGoogle Scholar
  6. 6.
    R. E. Bryant, D. L. Beatty, and C. H. Seger. Formal hardware verification by symbolic ternary trajectory evaluation. In Proc. of the Design Automation Conference, pages 397–402, 1991.Google Scholar
  7. 7.
    J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In Proc. of the Design Automation Conference, pages 46–51, June 1990.Google Scholar
  8. 8.
    G. Cabodi, P. Camurati, L. Lavagno, and S. Quer. Disjunctive partitionining and partial iterative squaring: An effective approach for symbolic traversal of large circuits. In Proc. of the Design Automation Conference, pages 728–733, Anaheim, CA, June 1997.CrossRefGoogle Scholar
  9. 9.
    G. Cabodi, P. Camurati, and S. Quer. Improved reachability analysis of large finite state machines. In Proc. of the International Conference on Computer-Aided Design, pages 354–360, Santa Clara, CA, November 1996.Google Scholar
  10. 10.
    E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla. Symmetry reductions in model checking. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV’98), pages 147–158. Springer-Verlag, Berlin, 1998. LNCS 1427.CrossRefGoogle Scholar
  11. 11.
    P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by constructions or approximation of fixpoints. In Proc. of the ACM Symposium on the Principles of Programming Languages, pages 238–250, 1977.Google Scholar
  12. 12.
    J. Desel and E. Kindler. Proving correctness of distributed algorithms using highlevel Petri nets: A case study. In International Conference on Application of Concurrency to System Design, Aizu, Japan, March 1998.Google Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    H. Iwashita, T. Nakata, and F. Hirose. CTL model checking based on forward state traversal. In Proc. of the International Conference on Computer-Aided Design, pages 82–87, San Jose, CA, November 1996.Google Scholar
  15. 15.
    M. Kaufmann, A. Martin, and C. Pixley. Design constraints in symbolic model checking. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV’98), pages 477–487. Springer-Verlag, Berlin, 1998. LNCS 1427.CrossRefGoogle Scholar
  16. 16.
    R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.Google Scholar
  17. 17.
    J. Lu and S. Tahar. On the verification and reimplementation of an ATM switch fabric using VIS. Technical Report 401, Concordia University, Department of Electrical and Computer Engineering, September 1997.Google Scholar
  18. 18.
    G. S. Manku, R. Hojati, and R. K. Brayton. Structural symmetry and model checking. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV’98), pages 159–171. Springer-Verlag, Berlin, 1998. LNCS 1427.CrossRefGoogle Scholar
  19. 19.
    K. L. McMillan. Symbolic Model Checking. Kluwer, Boston, MA, 1994.Google Scholar
  20. 20.
    K. L. McMillan. Personal Communication, February 1998.Google Scholar
  21. 21.
    K. L. McMillan. Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In A. J. Hu and M. Y. Vardi, editors, Tenth Conference on Computer Aided Verification (CAV’98), pages 110–121. Springer-Verlag, Berlin, 1998. LNCS 1427.CrossRefGoogle Scholar
  22. 22.
    A. Narayan, A. J. Isles, J. Jain, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Reachability analysis using partitioned ROBDDs. In Proc. of the International Conference on Computer-Aided Design, pages 388–393, November 1997.Google Scholar
  23. 23.
    R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. IWLS95, Lake Tahoe, CA., May 1995.Google Scholar
  24. 24.
    K. Ravi, K. L. McMillan, T. R. Shiple, and F. Somenzi. Approximation and decomposition of decision diagrams. In Proc. of the Design Automation Conference, pages 445–450, San Francisco, CA, June 1998.Google Scholar
  25. 25.
    K. Ravi and F. Somenzi. High-density reachability analysis. In Proc. of the International Conference on Computer-Aided Design, pages 154–158, San Jose, CA, November 1995.Google Scholar
  26. 26.
    K. Ravi and F. Somenzi. Efficient fixpoint computation for invariant checking. In Proc. of the International Conference on Computer Design, Austin, TX, October 1999. To appear.Google Scholar
  27. 27.
    R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. of the International Conference on Computer-Aided Design, pages 42–47, Santa Clara, CA, November 1993.Google Scholar
  28. 28.
    H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDD’s. In Proc. of the IEEE International Conference on Computer Aided Design, pages 130–133, November 1990.Google Scholar
  29. 29.
    C. H. Yang and D. L. Dill. Validation with guided search of the state space. In Proc. of the Design Automation Conference, pages 599–604, San Francisco, CA, June 1998.Google Scholar
  30. 30.
    J. Yuan, J. Shen, J. Abraham, and A. Aziz. On combining formal and informal verification. In O. Grumberg, editor, Ninth Conference on Computer Aided Verification (CAV’97), pages 376–387. Springer-Verlag, Berlin, 1997. LNCS 1254.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Kavita Ravi
    • 1
  • Fabio Somenzi
    • 2
  1. 1.Cadence Design SystemsUSA
  2. 2.Department of Electrical and Computer EngineeringUniversity of Colorado at BoulderUSA

Personalised recommendations