Exploration of sequential depth by evolutionary algorithms

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.