A SystemC-based framework for properties incompleteness evaluation

The use of model checking to validate descriptions of digital systems lacks a coverage metrics. How many properties has the verification engineer to define in order to assure the correctness of a design? An estimation methodology based on a high level fault model has been formally presented by A. Fedeli et al. (2003). It evaluates properties incompleteness. We propose a SystemC framework that implements the methodology in a completely automatic way. Experimental results highlight both the effectiveness of the methodology and the flexibility of the SystemC framework to measure the properties incompleteness on different kind of designs, which require different model checking approaches.