Partial Order Reduction for Timed Circuit Verification Based on Level Oriented Model

Tomoya KITAI
Yusuke OGURO
Tomohiro YONEDA
Eric MERCER
Chris MYERS

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E86-D    No.12    pp.2601-2611
Publication Date: 2003/12/01
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Issue on Dependable Computing)
Category: Verification and Dependability Analysis
Keyword: 
Level-oriented model,  timed asynchronous circuits,  formal verification,  time Petri nets,  

Full Text: PDF(1006.1KB)>>
Buy this Article



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.


open access publishing via