Modeling and validation of globally asynchronous design in synchronous frameworks

We lay a foundation for modeling and validation of asynchronous designs in a multi-clock synchronous programming model. This allows us to study properties of globally asynchronous systems using synchronous simulation and model-checking toolkits. Our approach can be summarized as automatic transformation of a design consisting of two asynchronously composed synchronous components into a fully synchronous multi-clock model preserving the flow equivalence. Since true asynchrony is not amenable to modeling in synchronous design frameworks, we seek to automatically insert desynchronizing protocol to 'match' the asynchronous model. Such protocol insertion brings about the possibility of formally investigating the behavior of globally asynchronous components in synchronous environments and hence leveraging the tools and techniques developed over decades for such environments. The ultimate goal of this research is to provide the possibility to model and build GALS systems in a way to preserve some proven properties when deployed on an asynchronous network.