Abstract
Verification has become one of the major bottlenecks in today’s circuit and system design. Up to 80% of the overall design costs are due to checking the correctness. Formal verification based on Bounded Model Checking (BMC) is a very powerful method that allows to prove the correctness of a device. In BMC the circuits behavior is considered over a finite time interval, but for the user it is often difficult to determine this interval for a given Device Under Verification (DUV).
In this paper we present a simulation based approach to automatically determine the sequential depth of a Finite State Machine (FSM) corresponding to the DUV. An Evolutionary Algorithm (EA) is applied to get high quality results. Experiments are given to demonstrate the efficiency of the approach.
Chapter PDF
Similar content being viewed by others
References
Ashar, P. and Malik, S. (1995). Fast functional simulation using branching programs. In Int’l Conf. on CAD, pages 408–412.
Bentley, B. (2001). Validating the Intel Pentium 4 microprocessor. In Design Automation Conf., pages 244–248.
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., and Zhu, Y. (1999). Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conf., pages 317–320.
Burch, J.R., Clarke, E.M., McMillan, K.L., and Dill, D.L. (1990). Sequential circuit verification using symbolic model checking. In Design Automation Conf., pages 46–51.
Corno, F., Prinetto, P., Rebaudengo, M., and Reorda, M.S. (1996a). GATTO: A genetic algorithm for automatic test pattern generation for large synchronous sequential circuits. IEEE Trans. on CAD, 15(8):991–1000.
Corno, F., Prinetto, P., Rebaudengo, M., Reorda, M.S., and Mosca, R. (1996b). Advanced techniques for GA-based sequential ATPG. In European Design & Test Conf., pages 375–379.
Davis, L. (1991). Handbook of Genetic Algorithms. van Nostrand Reinhold, New York.
Deb, K. (2001). Multi-objective Optimization using Evolutionary Algorithms. John Wiley and Sons, New York.
Drechsler, N., Drechsler, R., and Becker, B. (1999). A new model for multi-objective optimization in evolutionary algorithms. In Int’l Conference on Computational Intelligence (Fuzzy Days), volume 1625 of LNCS, pages 108–117. Springer Verlag.
Drechsler, R. and Drechsler, N. (2002). Evolutionary Algorithms for Embedded System Design. Kluwer Academic Publisher.
Goeckel, N., Drechsler, R., and Becker, B. (1997). GAME: A software environment for using genetic algorithms in circuit design. In Applications of Computer Systems, pages 240–247.
Keim, M., Drechsler, N., Drechsler, R., and Becker, B. (2001). Combining GAs and symbolic methods for high quality test of sequential circuits. Jour. of Electronic Testing: Theory and Applications, 17:141–142.
Mneimneh, M. and Sakallah, K. (2003). SAT-based sequential depth computation. In ASP Design Automation Conf.
Rudnick, E.M., Patel, J.H., Greenstein, G.S., and Niermann, T.M. (1997). Genetic algorithm framework for test generation. IEEE Trans. on CAD, 16(9): 1034–1044.
Somenzi, F. (2001). Efficient manipulation of decision diagrams. Software Tools for Technology Transfer, 3(2):171–181.
Yen, C.-C., Chen, K.-C., and Jou, J.-Y. (2002). A practical approach to cycle bound estimation for bounded model checking. In Int’l Workshop on Logic Synth., pages 149–154.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 International Federation for Information Processing
About this paper
Cite this paper
Drechsler, N., Drechsler, R. (2006). Exploration of Sequential Depth by Evolutionary Algorithms. In: Glesner, M., Reis, R., Indrusiak, L., Mooney, V., Eveking, H. (eds) VLSI-SOC: From Systems to Chips. IFIP International Federation for Information Processing, vol 200. Springer, Boston, MA. https://doi.org/10.1007/0-387-33403-3_5
Download citation
DOI: https://doi.org/10.1007/0-387-33403-3_5
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-33402-8
Online ISBN: 978-0-387-33403-5
eBook Packages: Computer ScienceComputer Science (R0)