algorithm design and analysis

State space reductions for scalable verification of asynchronous designs

This paper presents several state space reductions for verifying non-trivial asynchronous designs with a compositional minimization approach. These reductions result in a reduced model that contains the exact set of observably equivalent behavior. …

Hazard Checking of Timed Asynchronous Circuits Revisited

This paper proposes a new approach for the hazard checking of timed asynchronous circuits. Previous papers proposed either exact algorithms, which suffer from statespace explosion, or efficient algorithms which use a (conservative) approximation to …

Level oriented formal model for asynchronous circuit verification and its efficient analysis method

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, …

Direct synthesis of timed circuits from free-choice STGs

Presents a new method to synthesize timed asynchronous circuits directly from the specification without generating a state graph. The synthesis procedure begins with a graph specification with timing constraints. A timing analysis extracts the timed …

Timed circuit verification using TEL structures

Recent design examples have shown that significant performance gains are realized when circuit designers are allowed to make aggressive timing assumptions. Circuit correctness in these aggressive styles is highly timing dependent and, in industry, …

Direct synthesis of timed asynchronous 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 …

Direct synthesis of timed asynchronous 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 …

POSET timing and its application to the synthesis and verification of gate-level timed circuits

This paper presents a new algorithm for timed state-space exploration, POSET timing, POSET timing improves upon geometric methods by utilizing concurrency and causality information to dramatically reduce the number of geometric regions needed to …

Efficient timing analysis algorithms for timed state space exploration

This paper presents new timing analysis algorithms for efficient state space exploration during timed circuit synthesis. Timed circuits are a class of asynchronous circuits that incorporate explicit timing information in the specification which is …

Automatic synthesis of gate-level timed circuits with choice

This paper presents a CAD tool for the automatic synthesis of gate-level timed circuits from general specifications to basic gates such as AND gates, OR gates, and C-elements. Timed circuits are a class of asynchronous circuits that incorporate …