Exploiting clustering and decision-tree algorithms to mine LTL assertions containing non-boolean expressions

State-of-the-art mining tools generate assertions that either describe the temporal relations between Boolean expressions, or extract non-temporal logic formulas between more complex propositions involving arithmetic and/or relational operators. This paper presents a method for generating Linear Temporal Logic (LTL) assertions containing both the temporal dimension and the complexity of non-Boolean expressions. Starting from a set of simulation traces of the design under verification (DUV), our approach generates LTL assertions where the Boolean layer contains expressions of the form c = ne, c ≤ ne, c ≥ ne, c
l
≤ ne ≤ c
r
, where c, c
l
, c
r
are constants of numeric type, and ne is a numerical expression predicating over the variables of the DUV. The method exploits a clustering algorithm to mine a meaningful set of propositions following the aforementioned structure. After that, the propositions are used to generate temporal assertions through a decision tree algorithm. Experimental results show real improvements with respect to the state-of-the-art in terms of fault coverage and readability of the mined assertions.