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.
A SystemC-based Framework for Properties Incompleteness Evaluation
FIN, Alessandro;FUMMI, Franco;PONCINO, Massimo;PRAVADELLI, Graziano
2003-01-01
Abstract
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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
