Properties incompleteness evaluation by functional verification

Verification engineers cannot guarantee the correctness of the system implementation by model checking if the set of proven properties is incomplete. However, the use of model checking lacks widely accepted coverage metrics to evaluate the property completeness. The already existing metrics are based on time-consuming formal approaches that cannot be efficiently applied to medium/large systems. In this context, the paper proposes a coverage methodology based on a combination of static and dynamic verification that allows us to reduce the evaluation time with respect to pure formal approaches. The joining point between static and dynamic verification is represented by a fault model targeting functional descriptions. Functional fault simulation and dynamic automatic test pattern generation are used to quickly estimate the capability of properties in detecting functional faults. This provides a first estimation of the property completeness. Then, if necessary, model checking is used to complete the analysis, avoiding the underestimation of the property coverage that can be obtained due to the lack of exhaustiveness of dynamic verification. The proposed approach is theoretically founded and its effectiveness is compared with already existing techniques. In addition, experimental results to confirm the theoretical results are provided.