Assertion-based verification (ABV) is a promising approach for proving that the design implementation is consistent with the de- signer’s intents. However, ABV effectiveness depends on the quality of the assertions that are defined to capture the designer’s intents. As- sertions are generally defined by verification engineers that manually convert informal specifications in logic formulas according to their ex- pertise. However, manual definition is a time-consuming and error-prone activity, which may fail to exhaustively cover either the intended specifi- cation or the implemented behaviours. For this reason, different mining approaches have been recently proposed for the automatic generation of assertions. Unfortunately, in most cases, existing mining tools generate a set of over-constrained assertions. As a consequence, each assertion in the set is a long formula that describes a very specific behaviour of the design under verification (DUV). Thus, in the effort of covering as much DUV behaviours as possible, these approaches generate a huge amount of assertions with a negative impact on the total time required for their verification. To overcome this drawback, this paper introduces a dynamic approach that incrementally analyses control signals on DUV execution traces for mining more expressive temporal assertions that better cap- ture the I/O communication protocol. Then, to evaluate the effectiveness of the generated assertions in covering the intended behaviours, a tech- nique is proposed to estimate assertion’s interestingness by ranking them according to metrics typically adopted in the context of data mining.

Automatic Generation and Qualification of Assertions on Control Signals: A Time Window-Based Approach

DANESE, ALESSANDRO;GHASEMPOURI, TARA;PRAVADELLI, Graziano
2016

Abstract

Assertion-based verification (ABV) is a promising approach for proving that the design implementation is consistent with the de- signer’s intents. However, ABV effectiveness depends on the quality of the assertions that are defined to capture the designer’s intents. As- sertions are generally defined by verification engineers that manually convert informal specifications in logic formulas according to their ex- pertise. However, manual definition is a time-consuming and error-prone activity, which may fail to exhaustively cover either the intended specifi- cation or the implemented behaviours. For this reason, different mining approaches have been recently proposed for the automatic generation of assertions. Unfortunately, in most cases, existing mining tools generate a set of over-constrained assertions. As a consequence, each assertion in the set is a long formula that describes a very specific behaviour of the design under verification (DUV). Thus, in the effort of covering as much DUV behaviours as possible, these approaches generate a huge amount of assertions with a negative impact on the total time required for their verification. To overcome this drawback, this paper introduces a dynamic approach that incrementally analyses control signals on DUV execution traces for mining more expressive temporal assertions that better cap- ture the I/O communication protocol. Then, to evaluate the effectiveness of the generated assertions in covering the intended behaviours, a tech- nique is proposed to estimate assertion’s interestingness by ranking them according to metrics typically adopted in the context of data mining.
978-3-319-46096-3
assertion mining, assertion qualification, assertion-based verification
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/953303
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 2
social impact