Modeling and verification of globally asynchronous and locally synchronous ring architectures

The paper demonstrates a prevalent global deadlock situation resulting from a local deadlock in a GALS (globally asynchronous and locally synchronous) ring architecture. We present a novel design for building systems which are tolerant to such deadlocks arising in the local modules. The paper concentrates on the modeling of the proposed design methodology and its correctness is proved with the help of a public domain verification tool.