The biggest obstacle in the formal verification of large designs is their very large state spaces, which cannot be handled even by techniques such as implicit state space traversal. The only viable solution in most casesis validation byfunctionalsimulation. Unfortunately, this has the drawbacksof high computationalrequirements due to the large number of test vectors needed, and the lack of adequate coverage measures to characterize the quality of a given test set. To overcome these limitations, there has been recent interest in hybrid techniques which combine the strengths of formal verification and simulation. Formal verification-based techniques are used on a testmodel(usually muchsmaller thanthe design)to derive a set of functional test vectors, which are then used for design validation through simulation. The test set generated typically satisfies some coverage measure on the test model. Recent research has proposed the use of state or transition coverage. However, no effort h...