Toward Formalizing A Validation Methodology Using Simulation Coverage

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 cases is validation by functional simulation. Unfor-tunately, this has the drawbacksof high computational requirements due to the large number of test vectors needed, and the lack of ade-quate 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 verifica-tion and simulation. Formal verification-based techniques are used on a test model (usually much smaller than the 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 has been made to relate these measures to the coverage of design errors. Fur-thermore, the derivation of the test model remains largely ad-hoc, with few formal guidelines. We demonstrate that under a given set of assumptions, transition tours on test models can be used for complete validation of an im-plementation against a specification, for a large and important class of designs that includes many programmable/hardwired, general-purpose processors/DSPs. A by-product of this study is specific guidelines for deriving the test model, motivated by the require-ment of providing complete coverage of all errors. We illustrate the application of our methodology on a pipelined implementation of the DLX processor.