Analysing and closing simulation coverage by automatic generation and verification of formal properties from coverage reports

Tim Blackmore*, David Halliwell, Philip Barker, Kerstin Eder, Naresh Ramaram

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

2 Citations (Scopus)

Abstract

A significant amount of time during simulation-based hardware design verification is spent analysing coverage reports in order to identify which uncovered cases are coverable and which are not, ie indicating areas of dead code. This dead-code analysis is typically left until the code is stable because changes to the code can mean having to start the analysis again. Some formal tools offer a push-button functionality allowing this process to be automated to some extent. This paper extends this capability of formal tools. A method is presented that automatically extracts candidates for dead code analysis from coverage reports, turns these into formal assertions and uses a formal property checker to determine whether or not the code can be reached. The core principle of the method is based on temporal induction. The method is fully automatic and generic in that it can be implemented with any state-of-the-art formal property checker; it also does not need code stability. The major benefits of employing this method in practice are a saving of engineering effort and earlier coverage closure which can avoid late discovery of bugs and schedule slips.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages84-98
Number of pages15
Volume7321 LNCS
DOIs
Publication statusPublished - 2012
Event9th International Conference on Integrated Formal Methods, IFM 2012 - Pisa, Italy
Duration: 18 Jun 201221 Jun 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7321 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference9th International Conference on Integrated Formal Methods, IFM 2012
CountryItaly
CityPisa
Period18/06/1221/06/12

Fingerprint Dive into the research topics of 'Analysing and closing simulation coverage by automatic generation and verification of formal properties from coverage reports'. Together they form a unique fingerprint.

Cite this