Evaluating and Constraining Hardware Assertions with Absent Scenarios
- PDF / 757,582 Bytes
- 19 Pages / 595 x 842 pts (A4) Page_size
- 25 Downloads / 186 Views
Evaluating and Constraining Hardware Assertions with Absent Scenarios Hui-Na Chao1,2 , Hua-Wei Li1,2,3,∗ , Distinguished Member, CCF, Senior Member, IEEE Xiaoyu Song4 , Senior Member, IEEE, Tian-Cheng Wang1,2 , Member, CCF, and Xiao-Wei Li1,2 , Fellow, CCF, Senior Member, IEEE 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.
E-mail: {chaohuina, lihuawei}@ict.ac.cn; [email protected]; {wangtiancheng, lxw}@ict.ac.cn Received May 10, 2019; revised September 12, 2019. Abstract 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 -f ailRate 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. Keywords
1
hardware formal verification, assertion generation, data mining, assertion evaluation, assertion coverage
Introduction
In the domain of verifying integrated circuit, functional correctness is the essential requirement. Traditionally, simulation and formal verification are the main ways of functional verification. Simulation is a relatively mature and widely-used method in industry applications, but cannot perform complete verification. Formal verification, which can perform complete verification, requires a complete assertion set to cover the design’s functionality. If the assertion set is incomplete, more assertions should be generated. Consider the design that counts the occurrence of logic 1 within four continuous inputs of a primary input. The output is 1 if there are at least two logic 1s; otherwise, the output
is zero, i.e., O = (a ∨ Xa) ∧ (X 2 a ∨ X 3 a) ∨ (a ∧ Xa) ∨ (X 2 a ∧ X 3 a), where a is the one-bit input and O is the output. An assertion set A1 : (a = 0) ∧ X (a = 0) ∧ X 2 (a = 0) → X 3 (O = 0) , A2 : (a = 1) ∧ X 2 (a = 1) → X 3 (O = 1) , asserts that 1) starting from any instant, the output O is definitely logic 0 in the fourth cycle if there are three continuous 0s of input variable a
Data Loading...
