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

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.

Eric Mercer
Eric Mercer
Brigham Young University, Associate Professor
Chris Myers
Chris Myers
Department Chair / Professor

Related