Skip to main content
SpringerLink
Log in

Algorithms and Heuristics in VLSI Design

  • Chapter
  • First Online:
Experimental Algorithmics

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2547))

  • 684 Accesses

Abstract

The increasing complexity of nowadays VLSI designs makes it hard up to impossible to check their correctness by using validation methods like simulation. Therefore there is is a growing demand for formal verification methods in VLSI design and verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Aziz et al. Texas-97 benchmarks. http://www-cad.EECS.Berkeley.EDU/Respep/Research/Vis/texas-97.

  2. B. Bollig and I. Wegener, Improving the variable ordering of OBDDs is NP-complete. IEEE Transaction on Computers, 45(9):992–1002, 1996.

    Article  Google Scholar 

  3. R. K. Brayton, G. D. Hachtel, A. L. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. A. Edwards, S. P. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy and T. Villa. VIS: A System for Verification and Synthesis. In Proceedings of the Symposium on Computer Aided Verification (CAV’96), pages 428–432, 1996.

    Google Scholar 

  4. R. E. Bryant, Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35, pages 677–691, 1986.

    Article  Google Scholar 

  5. R.E. Bryant, On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Transaction on Computers, 40:205–213, 1991.

    Article  MathSciNet  Google Scholar 

  6. R. E. Bryant, Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992.

    Article  Google Scholar 

  7. J. R. Burch, E. M. Clarke and D. E. Long, Symbolic model checking with partitioned transition relations. In Proceedings of the International Conference on VLSI, pages 49–58, 1991.

    Google Scholar 

  8. J. R. Burch, E. M. Clarke, D. L. Dill, L. J. Hwang and K. L. McMillan, Symbolic model checking: 1020 states and beyond. In Proceedings of Logic in Computer Science (LICS’90), pages 428–439, 1990.

    Google Scholar 

  9. O. Coudert, C. Berthet and J. C. Madre, Verification of synchronous machines using symbolic execution. In Proceedings of the Workshop on Automatic Verification Methods for Finite State Machines. Springer Lecture Notes in Computer Science 407, pages 365–373, 1989.

    Google Scholar 

  10. O. Coudert and J. C. Madre, A unified framework for the formal verification of sequential circuits. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 126–129, 1990.

    Google Scholar 

  11. O. Coudert and J. C. Madre, The implicit set paradigm: a new approach to finite state system verification. Formal Methods in System Design, 6(2):133–145, 1995.

    Article  Google Scholar 

  12. S. J. Friedman and K. J. Supowit, Finding the optimal variable ordering for binary decision diagrams. IEEE Transactions on Computers, 39(5):710–713, 1990.

    Article  MathSciNet  Google Scholar 

  13. D. Geist and I. Beer, Efficient model checking by automated ordering of transition relation partitions. In Proceedings of Computer Aided Verification (CAV’94), pages 299–310, 1994.

    Google Scholar 

  14. R. Hojati, S. C. Krishnan, R. K. Brayton, Early qantification and partitioned transition relations. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 12–19, 1996.

    Google Scholar 

  15. R. D. M. Hunter and T. T. Johnson, Introduction to VHDL. Chapman & Hall, 1996.

    Google Scholar 

  16. S. Malik, A. R. Wang, R. K. Brayton, and A. Sangiovanni-Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In Proceedings of the 25th Design Automation Conference, pages 6–9, 1988.

    Google Scholar 

  17. K. L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  18. I. Moon, J. Jang, G. D. Hachtel, F. Somenzi, J. Yuan, and C. Pixley. Approximate reachability don’t cares for CTL model Checking. In Proceedings of the Internatuional Conference on CAD (ICCAD’98), 1998.

    Google Scholar 

  19. C. Meinel, K. Schwettmann, and A. Slobodová. Application driven variable reordering and an example implementation in reachabilityan alysis. In Proceedings of ASP-DAC’99, Hongkong, pages 327–330, 1999.

    Google Scholar 

  20. C. Meinel and C. Stangier. Speeding up image computation by using RTL information. In Proceedings of Formal Methods in CAD (FMCAD’00). Springer Lecture Notes in Computer Science 1954, pages 443–454, 2000.

    Google Scholar 

  21. C. Meinel and C. Stangier. Speeding up symbolic model checking by accelerating dynamic variable reordering. In Proceedings of the IEEE 10th Great Lakes Symopsium on VLSI, pages 39–42, 2000.

    Google Scholar 

  22. S. Minato, N. Ishiura, and S. Yahima. Shared binaryde cision diagrams with attributed edges for efficient Boolean function manipulation. In Proceedings of the 27th ACM/IEEE Design Automation Conference, pages 52–57, 1990.

    Google Scholar 

  23. R. K. Ranjan, A. Aziz, R. K. Brayton, C. Pixley, and B. Plessier. Efficient BDD algorithms for synthesizing and verifying finite state machines. Presented at the International Workshop on Logic Synthesis (IWLS’95), 1995.

    Google Scholar 

  24. R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proceedings of the ACM/IEEE International Conference on Computer-Aided Design, pages 42–47, 1993.

    Google Scholar 

  25. P. Savický and I. Wegener. Efficient algorithms for the transformation between different types of binary decision diagrams. Acta Informatica, 34:345–356, 1997.

    Google Scholar 

  26. D. Sieling. On the existence of polynomial time approximation schemes for OBDD minimization. In Proceedings of the 15th International Symposium on Theoretical Aspects of Computer Science (STACS’98). Springer Lecture Notes in Computer Science 1373, pages 205–215, 1998.

    Google Scholar 

  27. D. Sieling and I. Wegener. Reduction of BDDs in linear time. Information Processing Letters, 48(3):139–144, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  28. A. Slobodová and C. Meinel. Sample method for minimization of OBDDs. Presented at the International Workshop on Logic Synthesis, Tahoe City,CA, June 1998.

    Google Scholar 

  29. F. Somenzi. CUDD: CU Decision Diagram Package. http://vlsi.colorado.edu/pub/.

  30. S. Tani, K. Hamaguchi, and S. Yajima. The complexity of the optimal variable ordering problem of shared binary decision diagrams. In Proceedings of ISAAC’93. Springer Lecture Notes in Computer Science 762, pages 389–398, 1993.

    Google Scholar 

  31. D. E. Thomas and P. Moorby. The Verilog Hardware Description Language. Kluwer, 1991.

    Google Scholar 

  32. I. Wegener. Branching programs and binary decision diagrams-theory and applications. SIAM Monographs on Discrete Mathematics and Applications, 2000.

    Google Scholar 

  33. P. Woelfel. New bounds on the OBDD-size of integer multiplication via universal hashing. In Proceedings of STACS’01. Springer Lecture Notes in Computer Science 2010, 2001.

    Google Scholar 

  34. B. Yang. SMV models. http://www.cs.cmu.edu/~bwolen/software/, 1998.

  35. B. Yang, R. E. Bryant, D. R. O'Hallaron, A. Biere, O. Coudert, G. Janssen, R. K. Ranjan, and F. Somenzi. A performance study of BDD-based model checking. In Proceedings of Formal Methods in CAD (FMCAD’98), pages 255–289, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Trier, Trier, Germany

    Christoph Meinel & Christian Stangier

Authors
  1. Christoph Meinel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Stangier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Hong Kong University of Science and Technology, Clear Water Bay, Kowloon, Hong Kong

    Rudolf Fleischer

  2. Department of Computer Science, University of New Mexico, Farris Engineering Bldg, 87131-1386, Albuquerque, NM, USA

    Bernard Moret

  3. Department of Computer Science, University of Aarhus, Bld. 540, Ny Munkegade, 8000, Aarhus C, Denmark

    Erik Meineche Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Meinel, C., Stangier, C. (2002). Algorithms and Heuristics in VLSI Design. In: Fleischer, R., Moret, B., Schmidt, E.M. (eds) Experimental Algorithmics. Lecture Notes in Computer Science, vol 2547. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36383-1_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-36383-1_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00346-5

  • Online ISBN: 978-3-540-36383-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation