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

Abstract : Assertion-based verification (ABV) is a promising approach for proving that the design implementation is consistent with the designer’s intents. However, ABV effectiveness depends on the quality of the assertions that are defined to capture the designer’s intents. Assertions are generally defined by verification engineers that manually convert informal specifications in logic formulas according to their expertise. However, manual definition is a time-consuming and error-prone activity, which may fail to exhaustively cover either the intended specification 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 capture the I/O communication protocol. Then, to evaluate the effectiveness of the generated assertions in covering the intended behaviours, a technique is proposed to estimate assertion’s interestingness by ranking them according to metrics typically adopted in the context of data mining.
Type de document :
Communication dans un congrès
23th IFIP/IEEE International Conference on Very Large Scale Integration - System on a Chip (VLSI-SoC), Oct 2015, Daejeon, South Korea. IFIP Advances in Information and Communication Technology, AICT-483, pp.193-221, 2016, VLSI-SoC: Design for Reliability, Security, and Low Power. 〈10.1007/978-3-319-46097-0_10〉
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01578610
Contributeur : Hal Ifip <>
Soumis le : mardi 29 août 2017 - 14:46:06
Dernière modification le : mercredi 3 janvier 2018 - 11:32:31

Fichier

 Accès restreint
Fichier visible le : 2019-01-01

Connectez-vous pour demander l'accès au fichier

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Alessandro Danese, Francesca Filini, Tara Ghasempouri, Graziano Pravadelli. Automatic Generation and Qualification of Assertions on Control Signals: A Time Window-Based Approach. 23th IFIP/IEEE International Conference on Very Large Scale Integration - System on a Chip (VLSI-SoC), Oct 2015, Daejeon, South Korea. IFIP Advances in Information and Communication Technology, AICT-483, pp.193-221, 2016, VLSI-SoC: Design for Reliability, Security, and Low Power. 〈10.1007/978-3-319-46097-0_10〉. 〈hal-01578610〉

Partager

Métriques

Consultations de la notice

65