Partial Order Reduction for Timed Circuit Verification Based on Level Oriented Model
Summary :
Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines a level oriented formal model based on time Petri nets, and then proposes a partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.
- Publication
- IEICE TRANSACTIONS on Information Vol.E86-D No.12 pp.2601-2611
- Publication Date
- 2003/12/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on Dependable Computing)
- Category
- Verification and Dependability Analysis
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
Tomoya KITAI, Yusuke OGURO, Tomohiro YONEDA, Eric MERCER, Chris MYERS, "Partial Order Reduction for Timed Circuit Verification Based on Level Oriented Model" in IEICE TRANSACTIONS on Information,
vol. E86-D, no. 12, pp. 2601-2611, December 2003, doi: .
Abstract: Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines a level oriented formal model based on time Petri nets, and then proposes a partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.
URL: https://global.ieice.org/en_transactions/information/10.1587/e86-d_12_2601/_p
Copy
@ARTICLE{e86-d_12_2601,
author={Tomoya KITAI, Yusuke OGURO, Tomohiro YONEDA, Eric MERCER, Chris MYERS, },
journal={IEICE TRANSACTIONS on Information},
title={Partial Order Reduction for Timed Circuit Verification Based on Level Oriented Model},
year={2003},
volume={E86-D},
number={12},
pages={2601-2611},
abstract={Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines a level oriented formal model based on time Petri nets, and then proposes a partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.},
keywords={},
doi={},
ISSN={},
month={December},}
Copy
TY - JOUR
TI - Partial Order Reduction for Timed Circuit Verification Based on Level Oriented Model
T2 - IEICE TRANSACTIONS on Information
SP - 2601
EP - 2611
AU - Tomoya KITAI
AU - Yusuke OGURO
AU - Tomohiro YONEDA
AU - Eric MERCER
AU - Chris MYERS
PY - 2003
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E86-D
IS - 12
JA - IEICE TRANSACTIONS on Information
Y1 - December 2003
AB - Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines a level oriented formal model based on time Petri nets, and then proposes a partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.
ER -
English
