Skip to Main content Skip to Navigation

Modeling and Validation of Globally Asynchronous Design in Synchronous Frameworks

Abstract : 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.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:23:14 PM
Last modification on : Friday, January 8, 2021 - 3:40:39 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:31:00 PM


  • HAL Id : inria-00071644, version 1


Mohammad Reza Mousavi, Paul Le Guernic, Jean-Pierre Talpin, Sandeep Kumar Shukla, Twan Basten. Modeling and Validation of Globally Asynchronous Design in Synchronous Frameworks. [Research Report] RR-4935, INRIA. 2003. ⟨inria-00071644⟩



Record views


Files downloads