A parallelizable approach for mining likely invariants

A relevant aspect in design analysis and verification is mon- itoring how logic relations among di↵erent variables change at run time. Current static approaches su↵er from scalabil- ity problems that prevent their adoption on large designs. On the contrary, dynamic techniques scale better from the memory-consumption point of view. However, to achieve a high accuracy, they require to analyse a huge number of (long) execution traces, which results in time-consuming phases. In this paper, we present a new ecient approach to automatically infer logic relations among the variables of a design implementation. Both a sequential and a GPU- oriented parallel implementation are proposed to dynami- cally extract likely invariants from execution traces on dif- ferent time windows. Execution traces composed of millions of simulation instants can be eciently analysed.