Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Hal Ifip <>
Submitted on : Tuesday, August 29, 2017 - 2:46:06 PM
Last modification on : Tuesday, May 25, 2021 - 11:44:01 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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. pp.193-221, ⟨10.1007/978-3-319-46097-0_10⟩. ⟨hal-01578610⟩



Record views


Files downloads