Code coverage of assertions using RTL source code analysis

Viraj Athavale, Sai Ma, Samuel Hertz, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Assertions are gaining importance in pre-silicon hardware verification to ensure expected design behavior. Coverage of an assertion in terms of statements of a Register Transfer Level (RTL) source code is a very accessible metric for understanding the scope of assertions and for debug. However, few methods to report it currently exist. We present a methodology to define and compute code coverage of an assertion. Our method is based on static and dynamic analysis of the RTL source code. We demonstrate the scalability and effectiveness of our approach with experimental results on real designs for both manual and automatically generated assertions.

Original languageEnglish (US)
Title of host publicationDAC 2014 - 51st Design Automation Conference, Conference Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Print)9781479930173
DOIs
StatePublished - Jan 1 2014
Event51st Annual Design Automation Conference, DAC 2014 - San Francisco, CA, United States
Duration: Jun 2 2014Jun 5 2014

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X

Other

Other51st Annual Design Automation Conference, DAC 2014
CountryUnited States
CitySan Francisco, CA
Period6/2/146/5/14

Fingerprint

Assertion
Coverage
Static analysis
Dynamic analysis
Scalability
Hardware
Silicon
Static Analysis
Dynamic Analysis
Metric
Methodology
Experimental Results
Demonstrate
Design

Keywords

  • Assertions
  • Code coverage
  • Formal verification
  • Static analysis

ASJC Scopus subject areas

  • Computer Science Applications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering
  • Modeling and Simulation

Cite this

Athavale, V., Ma, S., Hertz, S., & Vasudevan, S. (2014). Code coverage of assertions using RTL source code analysis. In DAC 2014 - 51st Design Automation Conference, Conference Proceedings [2593108] (Proceedings - Design Automation Conference). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/2593069.2593108

Code coverage of assertions using RTL source code analysis. / Athavale, Viraj; Ma, Sai; Hertz, Samuel; Vasudevan, Shobha.

DAC 2014 - 51st Design Automation Conference, Conference Proceedings. Institute of Electrical and Electronics Engineers Inc., 2014. 2593108 (Proceedings - Design Automation Conference).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Athavale, V, Ma, S, Hertz, S & Vasudevan, S 2014, Code coverage of assertions using RTL source code analysis. in DAC 2014 - 51st Design Automation Conference, Conference Proceedings., 2593108, Proceedings - Design Automation Conference, Institute of Electrical and Electronics Engineers Inc., 51st Annual Design Automation Conference, DAC 2014, San Francisco, CA, United States, 6/2/14. https://doi.org/10.1145/2593069.2593108
Athavale V, Ma S, Hertz S, Vasudevan S. Code coverage of assertions using RTL source code analysis. In DAC 2014 - 51st Design Automation Conference, Conference Proceedings. Institute of Electrical and Electronics Engineers Inc. 2014. 2593108. (Proceedings - Design Automation Conference). https://doi.org/10.1145/2593069.2593108
Athavale, Viraj ; Ma, Sai ; Hertz, Samuel ; Vasudevan, Shobha. / Code coverage of assertions using RTL source code analysis. DAC 2014 - 51st Design Automation Conference, Conference Proceedings. Institute of Electrical and Electronics Engineers Inc., 2014. (Proceedings - Design Automation Conference).
@inproceedings{508c45ba40ea48b1bf11bdb7ff321eef,
title = "Code coverage of assertions using RTL source code analysis",
abstract = "Assertions are gaining importance in pre-silicon hardware verification to ensure expected design behavior. Coverage of an assertion in terms of statements of a Register Transfer Level (RTL) source code is a very accessible metric for understanding the scope of assertions and for debug. However, few methods to report it currently exist. We present a methodology to define and compute code coverage of an assertion. Our method is based on static and dynamic analysis of the RTL source code. We demonstrate the scalability and effectiveness of our approach with experimental results on real designs for both manual and automatically generated assertions.",
keywords = "Assertions, Code coverage, Formal verification, Static analysis",
author = "Viraj Athavale and Sai Ma and Samuel Hertz and Shobha Vasudevan",
year = "2014",
month = "1",
day = "1",
doi = "10.1145/2593069.2593108",
language = "English (US)",
isbn = "9781479930173",
series = "Proceedings - Design Automation Conference",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
booktitle = "DAC 2014 - 51st Design Automation Conference, Conference Proceedings",
address = "United States",

}

TY - GEN

T1 - Code coverage of assertions using RTL source code analysis

AU - Athavale, Viraj

AU - Ma, Sai

AU - Hertz, Samuel

AU - Vasudevan, Shobha

PY - 2014/1/1

Y1 - 2014/1/1

N2 - Assertions are gaining importance in pre-silicon hardware verification to ensure expected design behavior. Coverage of an assertion in terms of statements of a Register Transfer Level (RTL) source code is a very accessible metric for understanding the scope of assertions and for debug. However, few methods to report it currently exist. We present a methodology to define and compute code coverage of an assertion. Our method is based on static and dynamic analysis of the RTL source code. We demonstrate the scalability and effectiveness of our approach with experimental results on real designs for both manual and automatically generated assertions.

AB - Assertions are gaining importance in pre-silicon hardware verification to ensure expected design behavior. Coverage of an assertion in terms of statements of a Register Transfer Level (RTL) source code is a very accessible metric for understanding the scope of assertions and for debug. However, few methods to report it currently exist. We present a methodology to define and compute code coverage of an assertion. Our method is based on static and dynamic analysis of the RTL source code. We demonstrate the scalability and effectiveness of our approach with experimental results on real designs for both manual and automatically generated assertions.

KW - Assertions

KW - Code coverage

KW - Formal verification

KW - Static analysis

UR - http://www.scopus.com/inward/record.url?scp=84903172557&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84903172557&partnerID=8YFLogxK

U2 - 10.1145/2593069.2593108

DO - 10.1145/2593069.2593108

M3 - Conference contribution

SN - 9781479930173

T3 - Proceedings - Design Automation Conference

BT - DAC 2014 - 51st Design Automation Conference, Conference Proceedings

PB - Institute of Electrical and Electronics Engineers Inc.

ER -