Automatic Generation and Qualification of Assertions on Control Signals: A Time Window-Based Approach
Automatic Generation and Qualification of Assertions on Control Signals: A Time Window-Based Approach
复制标题
控制信号断言的自动生成和限定：基于时间窗口的方法
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
G. Pravadelli
中科院分区：
文献类型：
--
作者：
Alessandro Danese;Francesca Filini;Tara Ghasempouri;G. Pravadelli
基于断言的验证（ABV）是一种很有前途的方法来证明设计实现是符合设计者的意图。然而，ABV的有效性取决于断言的质量，这些断言被定义为捕获设计者的意图。断言通常由验证工程师定义，他们根据自己的专业知识手动转换逻辑公式中的非正式规范。然而，手动定义是一项耗时且容易出错的活动，可能无法完全涵盖预期的规范或实现的行为。出于这个原因，最近已经提出了不同的挖掘方法来自动生成断言。不幸的是，在大多数情况下，现有的挖掘工具生成一组过度约束的断言。因此，集合中的每个断言都是一个很长的公式，描述了验证中设计（DUV）的非常具体的行为。因此，在覆盖尽可能多的DUV行为的努力中，这些方法产生了大量的断言，对验证它们所需的总时间产生了负面影响。为了克服这个缺点，本文介绍了一种动态的方法，增量分析控制信号DUV执行轨迹挖掘更有表现力的时态断言，更好地捕捉I/O通信协议。然后，为了评估所生成的断言在覆盖预期行为的有效性，提出了一种技术来估计断言的兴趣度，根据通常采用的数据挖掘的上下文中的度量进行排名。
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.