This paper presents a compositional framework to address the state explosion problem in model checking of concurrent systems. This framework takes as input a system model described as a network of communicating components in a high-level description …
Using a level-oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model datapath circuits. On the other hand, in order to use such a model on large circuits, …
This paper presents a new method to synthesize timed asynchronous circuits directly from the specification without generating a state graph. The synthesis procedure begins with a deterministic graph specification with timing constraints. A timing …
This paper presents a new method to synthesize timed asynchronous circuits directly from the specification without generating a state graph. The synthesis procedure begins with a deterministic graph specification with timing constraints. A timing …