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

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.