Fourth International Workshop on
Formal Methods for Globally Asynchronous Locally Synchronous Design (FMGALS'09)

A DATE'09 Friday Workshop


April 24.,  Nice, France


FMGALS'09 is the 4th edition in a series of bi-annual workshops held in Pisa in 2003 (in conjunction with FME'03), in Verona in 2005 and Nice in 2007 (in conjunction with MEMOCODE'05 and MEMOCODE'07). Past workshop proceedings have been published with Elsevier's Electronic Notes in Theoretical Computer Science (ENTCS). Special issues of the Springer Journal Formal Methods in System Design and of the IEEE Design and Test magazine have been edited including most influential contributions to the workshop.


Sandeep K. Shukla, Virginia Polytechnic and State University, Blacksburg, USA
Jean-Pierre Talpin, INRIA Rennes-Bretagne-Atlantique, France


David Kinniment, University of Newcastle upon Tyne, UK

Invited Lecture

Ken Stevens, University of Utah



To bring together formal methods experts, asynchronous system designers and tools developers for GALS design. Identify scopes of formal methods in GALS design.


All aspects of research on GALS architecture including, but not limited to, models of computation, formal methods, modeling frameworks and tools, formal verification techniques, design automation, experimental results and case studies


Increasing cores and clock speed and decreasing engraving size of synchronous circuits raise taunting clock distribution and power leakage problems. For this reason, the Globally Asynchronous Locally Synchronous (GALS) model of computation has emerged as the paradigm of choice for SoC design with multiple timing domains, as well as for the software embedded on such circuits. Due to the inherent subtleties of asynchronous circuit design, formal methods are vital to make the GALS paradigm a success in the CAD industry. The FMGALS workshop aims at bringing together researchers from different communities interested in GALS design, and in applying formal methods in creating CAD tools enabling correct by construction GALS design.

FMGALS'09 invites papers on formal methods for GALS systems or that target any type of architecture combining synchronous and asynchronous notions of timing. Submissions reporting preliminary work are also encouraged. In particular, contributions are invited on the following topics, but not limited to:


The proceedings of the workshop will be published with Elsevier's Electronic Notes in Theoretical Computer Science (ENTCS).


Submissions shall be prepared in accordance with the ENTCS guidelines. The length of the initial submission is limited to the 15 pages in ENTCS format. Submitted manuscripts should be previously unpublished and should not have been concurrently submitted elsewhere. Submissions may be sent sent by e-mail to the workshop organizers.

Program Committee