Improving ABV by generation and abstraction of PSL assertions

Lo scopo di questa tesi è quello di fornire le metodologie efficienti per migliorare ABV in tre settori della generazione, astrazione e qualificazione delle asserzioni PSL. I principali contributi di questa tesi possono essere riassunti come segue: 1- una metodologia di estrazione automatica è stato proposta, per catturare le descrizioni del comportamento di un sistema in grado di generare un insiemi di asserzioni temporali da tracce di esecuzione. L'approccio è particolarmente adatto per asserzioni minerarie che descrive le relazioni aritmetiche tra ingressi e uscite secondo un insieme di pattern temporali. In comparazione con lo stato dell'arte, l'affermazione minatore proposto in questa metodologia, genera una serie di affermazioni di qualità più compatti e più alti. 2- una metodologia automatica astrazione che riutilizzare asserzioni originariamente definite per un dato IP RTL, per verificare il modello TLM corrispondente. La metodologia può essere diviso in due fasi principali, innanzitutto, asserzioni sintetizzate in metodi C ++ e in secondo luogo, inseriti nel modello TLM. I risultati mostrano che la metodologia può astrarre e riutilizzare le asserzioni da RTL a TLM ed evitare ridefinizione delle affermazioni che sono già esistenti a RTL. 3- una metodologia automatica qualificazione è stata proposta per valutare la qualità di asserzioni e per misurare la interestingness di asserzioni. L'approccio ri-adatta metriche da data mining per misurare la qualità delle asserzioni in base alla sua frequenza di attivazione durante simulazioni e la correlazione tra antecedente e conseguente. risultato sperimentale descrive la metodologia proposta fornisce una migliore stima di asserzioni interestingness.

The aim of this thesis is to provide efficient methodologies to improve ABV in three domains of generation, abstraction and qualification of PSL assertions. The main contributions of this thesis can be summarized as follows: 1- An automatic mining methodology has been proposed, for capturing behavioral descriptions of a system that can generate set of temporal assertions from execution traces. The approach is particularly suited for mining assertions that describes arithmetic relations between inputs and outputs according to a set of temporal patterns. In comparation with state of the art, assertion miner proposed in this methodology, generates a set of more compact and higher quality assertions. 2- An automatic abstraction methodology has been proposed to reuse assertions originally defined for a given RTL IP, to verify the corresponding TLM model. The methodology can be divided into two main phases, firstly, assertions synthesized into C++ methods and secondly, inserted in the TLM model. The results show that the methodology can abstract and reuse assertions from RTL to TLM and avoid redefinition of assertions which are already exist at RTL. 3- An automatic qualification methodology has been proposed to evaluate the quality of assertions to measure the interestingness of assertions. The approach re-adapts metrics from data mining to measure the quality of assertions based on its activation frequency during simulation runs and the correlation between antecedent and consequent. Experimental result depicts the proposed methodology provides a better estimation of assertions interestingness.