AI Chat Paper
Note: Please note that the following content is generated by AMiner AI. SciOpen does not take any responsibility related to this content.
{{lang === 'zh_CN' ? '文章概述' : 'Summary'}}
{{lang === 'en_US' ? '中' : 'Eng'}}
Chat more with AI
Powered by AMiner. Clicking this button will take you away from SciOpen.
Home Journal of Computer Science and Technology Article
Article Link
Cite
EndNote(RIS) BibTeX
Collect
Submit Manuscript
Show Outline
Outline
Show full outline
Hide outline
Outline
Show full outline
Hide outline
Regular Paper

Evaluating and Constraining Hardware Assertions with Absent Scenarios

State Key Laboratory of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences Beijing 100190, China
University of Chinese Academy of Sciences, Beijing 100049, China
Peng Cheng Laboratory, Shenzhen 518052, China
Department of Electrical and Computing Engineering, Portland State University, Portland, OR 97207, U.S.A.
Show Author Information

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-failRate 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

hardware formal verificationassertion generationdata miningassertion evaluationassertion coverage

Electronic Supplementary Material

Download File(s)
jcst-35-5-1198-Highlights.pdf (393.4 KB)

References

[1]
Vasudevan S, Sheridan D, Tcheng D, Tuohy B, Johnson D. GoldMine: Automatic assertion generation using data mining and static analysis. In Proc. the 13th Int. Conf. Design, Automation & Test in Europe, March 2010, pp.626-629.
Crossref
[2]

Hertz S, Sheridan D, Vasudevan S. Mining hardware assertions with guidance from static analysis. IEEE Trans. Computer Aided Design, 2013, 32(6): 952-965.
Crossref Google Scholar
[3]
Sheridan D, Liu L, Kim H, Vasudevan S. A coverage guided mining approach for automatic generation of succinct assertions. In Proc. the 27th Int. Conf. VLSI Design, January 2014, pp.68-73.
Crossref
[4]
Liu L, Lin C H, Vasudevan S. Word level feature discovery to enhance quality of assertion mining. In Proc. the 15th Int. Conf. Computer-Aided Design, March 2012, pp.210-217.
Crossref
[5]
Chang P, Wang L C. Automatic assertion extraction via sequential data mining of simulation traces. In Proc. the 15th Int. Conf. Asia and South Pacific Design Automation, January 2010, pp.607-612.
Crossref
[6]
Bertasi M, Guglielmo G, Pravadelli G. Automatic generation of compact formal properties for effective error detection. In Proc. the 11th Int. Conf. Hardware/Software Codesign and System Synthesis, September 2013, pp.1-10.
Crossref
[7]
Danese A, Ghasempouri T, Pravadelli G. Automatic extraction of assertions from execution traces of behavioural models. In Proc. the 18th Int. Conf. Design, Automation & Test in Europe, March 2015, pp.67–72.
Crossref
[8]
Danese A, Filini F, Pravadelli G. A time-window based approach for dynamic assertions mining on control signals. In Proc. the 23rd Int. Conf. Very Large Scale Integration, October 2015, pp. 246-251.
Crossref
[9]
Danese A, Pravadelli G, Zandonà I. Automatic generation of power state machines through dynamic mining of temporal assertions. In Proc. the 19th Int. Conf. Design, Automation & Test in Europe, March 2016, pp.606–611.
Crossref
[10]
Ciesielski M, Yu C, Brown W, Liu D. Verification of gate-level arithmetic circuits by function extraction. In Proc. the 52nd Int. Conf. Design Automation, June 2015.
Crossref
[11]
Hanafy M, Said H, Wahba A M. Complete properties extraction from simulation traces for assertions auto-generation. In Proc. the 24th Int. Conf. North Atlantic Test Workshop, May 2015.
Crossref
[12]
Hanafy M, Said H, Wahba A M. New methodology for digital design properties extraction from simulation traces. In Proc. the 10th Int. Conf. Computer Engineering & Systems, December 2015.
Crossref
[13]
Ghasempouri T, Pravadelli G. On the estimation of assertion interestingness. In Proc. the 23rd Int. Conf. Very Large Scale Integration, October 2015, pp.325-330.
Crossref
[14]

Mitra S, Banerjee A, Dasgupta P, Kumar H. Counterexample ranking using mined invariants. IEEE Trans. Computer Aided Design, 2013, 32(12): 1978–1991.
Crossref Google Scholar
[15]
Chao H, Li H, Song X, Wang T, Li X. On evaluating and constraining assertions using conflicts in absent scenarios. In Proc. the 26th Int. Conf. Asian Test Symposium, November 2017, pp.195-200.
Crossref
[16]

Ernst M, Cockrell J, Griswold W, Notkin D. Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Software Engineering, 2001, 27(2): 99–123.
Crossref Google Scholar
[17]
Hoskote Y, Kam T, Ho P H, Zhao X. Coverage estimation for symbolic model checking. In Proc. the 36th Int. Conf. Design Automation, June 1999, pp.300–305.
Crossref
[18]
Jayakumar N, Purandare M, Somenzi F. Dos and Don’ts of CTL state coverage estimation. In Proc. the 40th Int. Conf. Design Automation, June 2003, pp.292–295.
Crossref
[19]
Chao H, Li H, Wang T, Li X. An accurate algorithm for computing mutation coverage in model checking. In Proc. the 2016 IEEE International Test Conference, November 2016.
Crossref
[20]
Haedicke F, Große D, Drechsler R. A guiding coverage metric for formal verification. In Proc. the 15th Int. Conf. Design, Automation & Test in Europe, March 2012, pp.617- 622.
Crossref
[21]

Fedeli A, Fummi F, Pravadelli G. Properties incompleteness evaluation by functional verification. IEEE Trans. Computers, 2007, 56(4): 528-544.
Crossref Google Scholar
Journal of Computer Science and Technology
Volume 35 Issue 5,
September 2020
Pages 1198-1216
DOI: 10.1007/s11390-020-9708-x
Cite this article:
Chao H-N, Li H-W, Song X, et al. Evaluating and Constraining Hardware Assertions with Absent Scenarios. Journal of Computer Science and Technology, 2020, 35(5): 1198-1216. https://doi.org/10.1007/s11390-020-9708-x

456

Views

1

Crossref

N/A

Web of Science

1

Scopus

0

CSCD

Altmetrics
Received: 10 May 2019
Revised: 12 September 2019
Published: 30 September 2020
©Institute of Computing Technology, Chinese Academy of Sciences 2020
Return