An Error Simulation Based Approach to Measure Error Coverage of Formal Properties

Many approaches have been proposed for digital system ver-i¯cation, either based on simulation strategies or on formal veri¯cation techniques. Both of them show advantages and drawbacks and new mixed approaches have been presented in order to improve the veri¯cation process. Speci¯cally, the adoption of formal methods still lacks a coverage metrics to let the veri¯cation engineer get a measure of which portion of the circuit is already covered by the written properties that far and which parts still need to be addressed. The present paper describes a new simulation based methodology aimed at measuring the error coverage achieved by temporal as-sertions proved by model checking. The approach has been applied to the description of a protocol converter block, and some preliminary results are presented in the paper. 1