The ever increasing clock speed coupled with the ever 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'2007 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:

• formal design and synthesis techniques for GALS
• GALS model of computation for software architectures
• architectural transformations and equivalences
• formal verification of GALS systems
• formal methods for analysis of GALS systems
• hardware compilation of GALS system
• latency-insensitive synchronous systems
• mixed synchronous-asynchronous systems
• synchronous/asynchronous interaction
• clocking, interconnect and interface issues
• interfaces between multiple timing domains
• system decomposition into GALS architectures
• formal aspects of SoC and NoC design
• case studies, comparisons, and applications.

Proceedings of the FMGALS workshop will be published with Elsevier in the Electronic Notes on Theoretical Computer Science series (ENTCS). A selection of the best papers will be considered for publication in IEEE Design & Test, Special Issue on Globally Asynchronous and Locally Synchronous Design and Test (the deadline for this special issue will be specially postponed for the selected FMGALS papers).