explosion

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 …

Efficient Verification of Hazard-Freedom in Gate-Level Timed Asynchronous Circuits

This paper presents an efficient method for verifying hazard-freedom in gate-level timed asynchronous circuits. Timed circuits are a class of asynchronous circuits that are optimized using explicit timing information. In asynchronous circuits, …

Verification of timed circuits with failure-directed abstractions

This paper presents a method to address state explosion in timed-circuit verification by using abstraction directed by the failure model. This method allows us to decompose the verification problem into a set of subproblems, each of which proves that …

Efficient verification of hazard-freedom in gate-level timed asynchronous circuits

This paper presents an efficient method for verifying hazard freedom in timed asynchronous circuits. Timed circuits are a class of asynchronous circuits that utilize explicit timing information for optimization throughout the entire design process. …

Modular verification of timed circuits using automatic abstraction

The major barrier that prevents the application of formal verification to large designs is state explosion. This paper presents a new approach for verification of timed circuits using automatic abstraction. This approach partitions the design into …

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 state space exploration using POSETs

This paper presents a new timing analysis algorithm for efficient state space exploration during the synthesis of timed circuits or the verification of timed systems. The source of the computational complexity in the synthesis or verification of a …

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 …