This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Properties Incompleteness Evaluation by Functional Verification
April 2007 (vol. 56 no. 4)
pp. 528-544
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.
Index Terms:
Model checking, property coverage, functional verification, fault models.
Citation:
Andrea Fedeli, Franco Fummi, Graziano Pravadelli, "Properties Incompleteness Evaluation by Functional Verification," IEEE Transactions on Computers, vol. 56, no. 4, pp. 528-544, April 2007, doi:10.1109/TC.2007.1012
Usage of this product signifies your acceptance of the Terms of Use.