We present a simulation-based semiformal verification method for sequential circuits described at the register-transfer level. The method consists of an iterative loop where coverage analysis guides input pattern generation. An observability-based coverage metric is used to identify portions of the circuit not exercised by simulation. A heuristic algorithm then selects probability distributions for biased random input pattern generation that targets non-covered portions. This algorithm is based on an approximate analysis of the circuit modeled as a Markov chain at steady state. Node controllabilities and observabilities are estimated using a limited depth reconvergence analysis and an implicit algorithm for manipulating probability distributions and determining steady-state behavior An optimization algorithm iteratively perturbs the probability distributions of the primary inputs in order to improve estimated coverage. The coverage enhancement achieved by our approach is demonstrated on benchmarks from the ISCA589 and VIS suites.
展开▼
