Enhancing quality of assertion generation: methods for automatic assertion generation and evaluation

assertion;assertion generation;assertion evaluation;assertion ranking;GoldMine;static analysis;data mining;evaluation;ranking;verification;validation

Hertz, Samuel ; Vasudevan ; Shobha

关键词: assertion;    assertion generation;    assertion evaluation;    assertion ranking;    GoldMine;    static analysis;    data mining;    evaluation;    ranking;    verification;    validation;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/55156/Samuel_Hertz.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

We present methods for automatically generating and evaluating register transfer level (RTL) assertions. We detail the GoldMine methodology and each of its data mining algorithms. We introduce the Best-Gain Decision Forest algorithm to mine concise RTL assertions. We develop an assertion ranking methodology. We define assertion importance, complexity, rank and ideality and we detail methods to compute each of them. We present a case study and experimental results to demonstrate the effectiveness of assertion rank. We develop an assertion rank aggregation methodology. We define assertion coverage and expectedness. We aggregate rankings for assertion importance, complexity, coverage and expectedness. We present experimental results to demonstrate the value of these metrics and the rank aggregation methodology. We rigorously analyze the performance of each data mining algorithm in GoldMine. We present experimental results that demonstrate each algorithm's performance with respect to various metrics.