Likely invariants model properties that hold in operating conditions of a computing system. Dynamic mining of invariants aims at extracting logic formulas representing such properties from the system execution traces, and it is widely used for verification of intellectual property (IP) blocks. Although the extracted formulas represent likely invariants that hold in the considered traces, there is no guarantee that they are true in general for the system under verification. As a consequence, to increase the probability that the mined invariants are true in general, dynamic mining has to be performed to large sets of representative execution traces. This makes the execution-based mining process of actual IP blocks very time-consuming due to the trace lengths and to the large sets of monitored signals. This article presents Mangrove, an efficient implementation of a dynamic invariant mining algorithm for GPU architectures. Mangrove exploits inference rules, which are applied at run time to filter invariants from the execution traces and, thus, to sensibly reduce the problem complexity. Mangrove allows users to define invariant templates and, from these templates, it automatically generates kernels for parallel and efficient mining on GPU architectures. The article presents the tool, the analysis of its performance, and its comparison with the best sequential and parallel implementations at the state of the art.

We present a three-step flow to improve Assertion-based Verification methodology with integrated RTL-to-TLM abstraction: First, an automatic assertion miner generates a large set of possible assertions from an RTL design. Second, automatic assertion qualification identifies the most interesting assertions from this set. Third, the assertions are abstracted to the transaction level, such that they can be re-used in TLM verification. We show that the proposed flow automatically chooses the best assertions among the ones generated to verify the design components when abstracted from RTL to TLM. Our experimental results indicate that the proposed methodology allows us to re-use the most interesting set at TLM without relying on any time consuming or error-prone manual transformations with a considerable amount of speed up and considerable reduction in the execution time.

Several approaches exist for specification mining of hardware designs, both at the RTL and system levels (e.g, TLM). These approaches mine assertions that specify the behavior of the design. Some of the techniques require the source code itself while others can extract assertions directly from simulation traces. The performance of some approaches is highly dependent on the number of simulation traces/use cases while there exist approaches which can extract assertions from a limited number of simulation traces. Apart from this aspect, the core of each assertion miner is different from the other ones. Some use expression templates to define assertions while some are based on the static analysis or information flow analysis. Unfortunately, it has been rarely considered which of the current approaches are more effective in describing functionality of particular types of designs. Thus, in this work, we analyze assertion miners which are template based and dynamic dependency graph based, respectively. We generate assertions from both approaches. The evaluation considers fault analysis on both assertion sets of extracted assertions. Moreover, both sets are combined and fault analysis has been applied on them. Experimental results show that each set approximately detects the same number of faults while when the two sets are combined the number of detected faults increases. Finally, a new, more efficient architecture for an effective assertion miner has been developed based on the study in this work.

This paper presents DOVE, a validation framework to identify points of vulnerability inside IP firmwares. The framework relies on the symbolic simulation of the firmware to search for corner cases in its computational paths that may hide vulnerabilities. Then, DOVE automatically mine a compact set of formal assertions representing these unlikely paths to guide the analysis of the verification engineers. Experimental results on two case studies show the effectiveness of the generated assertions in pinpointing actual vulnerabilities and its efficiency in terms of execution time.

Different mining approaches have been proposed in literature for the automatic generation of temporal assertions from execution traces of digital systems. However, in most cases, existing tools can only mine assertions compliant with a limited set of pre-defined templates. Furthermore, they tend to generate a huge amount of assertions, while they still lack an effective way to measure their coverage in terms of design behaviours. To fill in the gap, this paper presents A-TEAM, a tool for the automatic extraction of temporal assertions starting from a set of user-defined assertion templates. Our method involves a combination of data mining and coverage analysis for mining a compact and expressive set of LTL formulas.

Dynamic mining of invariants is a class of approaches to extract logic formulas from the execution traces of a system under verification (SUV), with the purpose of expressing stable conditions in the behaviour of the SUV. The mined formulas represent likely invariants for the SUV, which certainly hold on the considered traces, but there is no guarantee that they are true in general. A large set of representative execution traces must be analysed to increase the probability that mined invariants are generally true. However, this becomes extremely time-consuming for current sequential approaches when long execution traces and large set of SUV variables are considered. To overcome this limitation, the paper presents a parallel approach for invariant mining that exploits GPU architectures for processing an execution trace composed of millions of clock cycles in few seconds.

Different mining approaches have been proposed in the past for automatic generation of assertions. However, in most cases, existing 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, we introduce 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. Experimental results show that our approach allows generating a compact set of assertions without penalizing the coverage of DUV behaviours.