The definition of assertions is a fundamental phase for formal and semi-formal verification strategies as well as for documenting purposes. Assertions are generally manually defined, but several (semi-) automatic approaches have been also proposed that mine assertions directly from execution traces of the design under verification (DUV). In both cases, assertion qualification is necessary to evaluate the quality of the defined assertions. Current approaches evaluate the interestingness of a set of assertions by measuring the percentage of DUV’s be- haviours covered by the assertions, mainly by adopting techniques based on mutation analysis, which require long simulation time. On the contrary, this work proposes an automatic technique to estimate the interestingness of assertions by ranking them according to metrics typically adopted in the context of data mining, which reveals to be a faster approach. Experimental results that compare the proposed assertion ranking strategy with assertion qualification based on mutation analysis are reported.
On the estimation of assertion interestingness
GHASEMPOURI, TARA;PRAVADELLI, Graziano
2015-01-01
Abstract
The definition of assertions is a fundamental phase for formal and semi-formal verification strategies as well as for documenting purposes. Assertions are generally manually defined, but several (semi-) automatic approaches have been also proposed that mine assertions directly from execution traces of the design under verification (DUV). In both cases, assertion qualification is necessary to evaluate the quality of the defined assertions. Current approaches evaluate the interestingness of a set of assertions by measuring the percentage of DUV’s be- haviours covered by the assertions, mainly by adopting techniques based on mutation analysis, which require long simulation time. On the contrary, this work proposes an automatic technique to estimate the interestingness of assertions by ranking them according to metrics typically adopted in the context of data mining, which reveals to be a faster approach. Experimental results that compare the proposed assertion ranking strategy with assertion qualification based on mutation analysis are reported.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.