Coverage estimation using transition perturbation for symbolic model checking in hardware verification

Xingwen Xu, Shinji Kimura, Kazunari Horikawa, Takehiko Tsuchiya

Research output: Contribution to journalArticle

Abstract

Lack of complete formal specification is one of the major obstacles to the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. Our coverage metric pinpoints the transitions through which the values of signals are checked. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

Original languageEnglish
Pages (from-to)3451-3457
Number of pages7
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
VolumeE89-A
Issue number12
DOIs
Publication statusPublished - 2006 Dec

Fingerprint

Symbolic Model Checking
Model checking
Coverage
Hardware
Perturbation
Model Checking
Cache Coherence
Network protocols
Metric
Formal Specification
Completeness
Estimator
Subset
Computing
Evaluate

Keywords

  • Model checking
  • Transition coverage

ASJC Scopus subject areas

  • Electrical and Electronic Engineering
  • Hardware and Architecture
  • Information Systems

Cite this

Coverage estimation using transition perturbation for symbolic model checking in hardware verification. / Xu, Xingwen; Kimura, Shinji; Horikawa, Kazunari; Tsuchiya, Takehiko.

In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E89-A, No. 12, 12.2006, p. 3451-3457.

Research output: Contribution to journalArticle

@article{1bf59732ea9a4ea09954974bf51ea299,
title = "Coverage estimation using transition perturbation for symbolic model checking in hardware verification",
abstract = "Lack of complete formal specification is one of the major obstacles to the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. Our coverage metric pinpoints the transitions through which the values of signals are checked. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.",
keywords = "Model checking, Transition coverage",
author = "Xingwen Xu and Shinji Kimura and Kazunari Horikawa and Takehiko Tsuchiya",
year = "2006",
month = "12",
doi = "10.1093/ietfec/e89-a.12.3451",
language = "English",
volume = "E89-A",
pages = "3451--3457",
journal = "IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences",
issn = "0916-8508",
publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
number = "12",

}

TY - JOUR

T1 - Coverage estimation using transition perturbation for symbolic model checking in hardware verification

AU - Xu, Xingwen

AU - Kimura, Shinji

AU - Horikawa, Kazunari

AU - Tsuchiya, Takehiko

PY - 2006/12

Y1 - 2006/12

N2 - Lack of complete formal specification is one of the major obstacles to the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. Our coverage metric pinpoints the transitions through which the values of signals are checked. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

AB - Lack of complete formal specification is one of the major obstacles to the deployment of model checking. Coverage estimation addresses this issue by revealing the unverified part of the design according to the specified properties. In this paper we propose a new transition-based coverage metric to evaluate the completeness of properties for symbolic model checking. Our coverage metric pinpoints the transitions through which the values of signals are checked. An efficient symbolic algorithm is presented for computing the transition coverage for a subset of ACTL. Our coverage estimator has been applied to the model checking of a cache coherence protocol. We uncovered several coverage holes including one that eventually led to the discovery of a design bug.

KW - Model checking

KW - Transition coverage

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

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

U2 - 10.1093/ietfec/e89-a.12.3451

DO - 10.1093/ietfec/e89-a.12.3451

M3 - Article

AN - SCOPUS:33845587371

VL - E89-A

SP - 3451

EP - 3457

JO - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

JF - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

SN - 0916-8508

IS - 12

ER -