Improving simulation-based verification by means of formal methods

The design of complex systems is largely ruled by the time needed for verification. Even though formal methods can provide higher reliability, in practice often simulation based verification is used. Large testbenches are created and if the design produces the correct output for all stimuli it is said to be correct. But there is no guarantee that the testbench is complete in the sense that it contains test-cases for all ??important?? situations. We propose an approach to detect ??gaps?? in testbenches, i.e. behavior that is not tested. The approach relies on automatic generation of properties from the testbench in terms of a formal property language. By construction the properties are valid within the testbench. A model checker proves the validity of the property on the design. If this proof succeeds, the testbench covers all possible situations for given signals. In case of failure counter-examples are produced. These counter-examples represent behavior that is not tested, i.e. a gap in the testhench. The feasibility of the approach is underlined by experiments.