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.
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Aziz et al. Texas-97 benchmarks. http://www-cad.EECS.Berkeley.EDU/Respep/Research/Vis/texas-97.
B. Bollig and I. Wegener, Improving the variable ordering of OBDDs is NP-complete. IEEE Transaction on Computers, 45(9):992–1002, 1996.
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.
R. E. Bryant, Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35, pages 677–691, 1986.
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.
R. E. Bryant, Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992.
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.
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.
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.
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.
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.
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.
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.
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.
R. D. M. Hunter and T. T. Johnson, Introduction to VHDL. Chapman & Hall, 1996.
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.
K. L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993.
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.
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.
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.
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.
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.
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.
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.
P. Savický and I. Wegener. Efficient algorithms for the transformation between different types of binary decision diagrams. Acta Informatica, 34:345–356, 1997.
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.
D. Sieling and I. Wegener. Reduction of BDDs in linear time. Information Processing Letters, 48(3):139–144, 1993.
A. Slobodová and C. Meinel. Sample method for minimization of OBDDs. Presented at the International Workshop on Logic Synthesis, Tahoe City,CA, June 1998.
F. Somenzi. CUDD: CU Decision Diagram Package. http://vlsi.colorado.edu/pub/.
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.
D. E. Thomas and P. Moorby. The Verilog Hardware Description Language. Kluwer, 1991.
I. Wegener. Branching programs and binary decision diagrams-theory and applications. SIAM Monographs on Discrete Mathematics and Applications, 2000.
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.
B. Yang. SMV models. http://www.cs.cmu.edu/~bwolen/software/, 1998.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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