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.

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

Germiniani, Samuele;Pravadelli, Graziano
2022-01-01

Abstract

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.
2022
978-1-6654-9005-4
Decision trees
Assertion mining
Temporal assertions
Clustering algorithms
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1079517
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact