Improvements in Coverability Analysis.

In simulation-based verification users are faced with the challenge of maximizing test coverage while minimizing testing costs. Sophisticated techniques are used to generate clever test cases and to determine the quality attained by the tests. The latter activity, which is essential for locating areas of the design that need to have more tests, is called test coverage analysis.We have previously introduced the notion of coverability, which refers to the degree to which a model can be covered when subjected to testing. We showed how a coverability analyzer enables naive users to take advantage of the power of symbolic model checking with a 'one-button' interface for coverability analysis. In this work, we present several heuristics, based on static program analysis and on simulation of counter examples, for improving the efficiency of coverability analysis by symbolic model checking. We explain each heuristic independently and suggest a way to combine them. We present an experiment that shows improvements based on using random simulation in the analysis of coverability.