Evaluating and Constraining Hardware Assertions with Absent Scenarios  

作　　者：Hui-Na Chao Hua-Wei Li Xiaoyu Song Tian-Cheng Wang Xiao-Wei Li 

机构地区：[1]State Key Laboratory of Computer Architecture,Institute of Computing Technology,Chinese Academy of Sciences Beijing 100190,China [2]University of Chinese Academy of Sciences,Beijing 100049,China [3]Peng Cheng Laboratory,Shenzhen 518052,China [4]Department of Electrical and Computing Engineering,Portland State University,Portland,OR 97207,U.S.A.

出　　处：《Journal of Computer Science & Technology》2020年第5期1198-1216,共19页计算机科学技术学报（英文版）

基　　金：supported in part by the National Natural Science Foundation of China under Grant Nos.61876173,61432017,and 61532017.

摘　　要：Mining from simulation data of the golden model in hardware design verification is an effective solution to assertion generation.While the simulation data is inherently incomplete,it is necessary to evaluate the truth values of the mined assertions.This paper presents an approach to evaluating and constraining hardware assertions with absent scenarios.A Belief-fail Rate metric is proposed to predict the truth/falseness of generated assertions.By considering both the occurrences of free variable assignments and the conflicts of absent scenarios,we use the metric to sort true assertions in higher ranking and false assertions in lower ranking.Our Belief-failRate guided assertion constraining method leverages the quality of generated assertions.The experimental results show that the Belief-failRate framework performs better than the existing methods.In addition,the assertion evaluating and constraining procedure can find more assertions that cover new design functionality in comparison with the previous methods.

关 键 词：hardware formal verification assertion generation data mining assertion evaluation assertion coverage 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]