Automated Test Generation for Activation of Assertions in RTL Models

Yangdi Lyu; Prabhat Mishra

Automated Test Generation for Activation of Assertions in RTL Models

Yangdi Lyu, Prabhat Mishra

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

Abstract

A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously.

Original language	English
Title of host publication	ASP-DAC 2020 - 25th Asia and South Pacific Design Automation Conference, Proceedings
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	223-228
Number of pages	6
ISBN (Electronic)	9781728141237
Publication status	Published - Jan 2020
Externally published	Yes
Event	25th Asia and South Pacific Design Automation Conference, ASP-DAC 2020 - Beijing, China Duration: 13 Jan 2020 → 16 Jan 2020

Publication series

Name	Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
Volume	2020-January

Conference

Conference	25th Asia and South Pacific Design Automation Conference, ASP-DAC 2020
Country/Territory	China
City	Beijing
Period	13/01/20 → 16/01/20

Bibliographical note

Publisher Copyright:
© 2020 IEEE.

Access to Document

https://hdl.handle.net/1783.1/121152

Cite this

Lyu, Y., & Mishra, P. (2020). Automated Test Generation for Activation of Assertions in RTL Models. In ASP-DAC 2020 - 25th Asia and South Pacific Design Automation Conference, Proceedings (pp. 223-228). Article 9045731 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC; Vol. 2020-January). Institute of Electrical and Electronics Engineers Inc.. https://hdl.handle.net/1783.1/121152

@inproceedings{28ea291c6d56417b9eeecc4271e97152,

title = "Automated Test Generation for Activation of Assertions in RTL Models",

abstract = "A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously.",

author = "Yangdi Lyu and Prabhat Mishra",

note = "Publisher Copyright: {\textcopyright} 2020 IEEE.; 25th Asia and South Pacific Design Automation Conference, ASP-DAC 2020 ; Conference date: 13-01-2020 Through 16-01-2020",

year = "2020",

month = jan,

language = "English",

series = "Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "223--228",

booktitle = "ASP-DAC 2020 - 25th Asia and South Pacific Design Automation Conference, Proceedings",

}

Lyu, Y & Mishra, P 2020, Automated Test Generation for Activation of Assertions in RTL Models. in ASP-DAC 2020 - 25th Asia and South Pacific Design Automation Conference, Proceedings., 9045731, Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC, vol. 2020-January, Institute of Electrical and Electronics Engineers Inc., pp. 223-228, 25th Asia and South Pacific Design Automation Conference, ASP-DAC 2020, Beijing, China, 13/01/20. <https://hdl.handle.net/1783.1/121152>

Automated Test Generation for Activation of Assertions in RTL Models. / Lyu, Yangdi; Mishra, Prabhat.
ASP-DAC 2020 - 25th Asia and South Pacific Design Automation Conference, Proceedings. Institute of Electrical and Electronics Engineers Inc., 2020. p. 223-228 9045731 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC; Vol. 2020-January).

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

TY - GEN

T1 - Automated Test Generation for Activation of Assertions in RTL Models

AU - Lyu, Yangdi

AU - Mishra, Prabhat

PY - 2020/1

Y1 - 2020/1

N2 - A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously.

AB - A major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously.

UR - https://www.scopus.com/pages/publications/85083024592

M3 - Conference Paper published in a book

AN - SCOPUS:85083024592

T3 - Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

SP - 223

EP - 228

BT - ASP-DAC 2020 - 25th Asia and South Pacific Design Automation Conference, Proceedings

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 25th Asia and South Pacific Design Automation Conference, ASP-DAC 2020

Y2 - 13 January 2020 through 16 January 2020

ER -

Automated Test Generation for Activation of Assertions in RTL Models

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this