Coverage Estimation Using Transition Perturbation for Symbolic Model Checking in Hardware Verification
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E89-A No.12 pp.3451-3457
- Publication Date
- 2006/12/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1093/ietfec/e89-a.12.3451
- Type of Manuscript
- Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
- Category
- Simulation and Verification
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Xingwen XU, Shinji KIMURA, Kazunari HORIKAWA, Takehiko TSUCHIYA, "Coverage Estimation Using Transition Perturbation for Symbolic Model Checking in Hardware Verification" in IEICE TRANSACTIONS on Fundamentals,
vol. E89-A, no. 12, pp. 3451-3457, December 2006, doi: 10.1093/ietfec/e89-a.12.3451.
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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1093/ietfec/e89-a.12.3451/_p
Copy
@ARTICLE{e89-a_12_3451,
author={Xingwen XU, Shinji KIMURA, Kazunari HORIKAWA, Takehiko TSUCHIYA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Coverage Estimation Using Transition Perturbation for Symbolic Model Checking in Hardware Verification},
year={2006},
volume={E89-A},
number={12},
pages={3451-3457},
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={},
doi={10.1093/ietfec/e89-a.12.3451},
ISSN={1745-1337},
month={December},}
Copy
TY - JOUR
TI - Coverage Estimation Using Transition Perturbation for Symbolic Model Checking in Hardware Verification
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 3451
EP - 3457
AU - Xingwen XU
AU - Shinji KIMURA
AU - Kazunari HORIKAWA
AU - Takehiko TSUCHIYA
PY - 2006
DO - 10.1093/ietfec/e89-a.12.3451
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E89-A
IS - 12
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - December 2006
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.
ER -
English
