Compositional synthesis of latency-insensitive systems from multi-clocked synchronous specifications
Résumé
We consider the problem of synthesizing correct-by-construction globally asynchronous, locally synchronous (GALS) implementations from modular synchronous specifications. This involves the synthesis of asynchronous wrappers that drive the synchronous clocks of the modules and perform input reading in such a fashion as to preserve, in a certain sense, the global properties of the system. Our approach is based on the weakly endochronous synchronous model, which gives criteria guaranteeing the existence of simple and efficient asynchronous wrappers. We focus on the transformation (by means of added signalling) of the synchronous modules of a multiclock synchronous specification into weakly endochronous modules, for which simple and efficient wrappers exist. // Nous considérons le problème de transformer une spécification fonctionnelle synchrone multi-horloge en une mise en oeuvre globallement asynchrone de manière modulaire et correcte par construction. Pour cela, nous élaborons une technique de compilation permettant de transformer une spécification déclarative synchrone en un automate effectuant des opérations atomiques de lecture, de calcul et d'écriture et assurant un invariant global d'insensibilité à la latence tout en préservant les propriétés locales de la spécification initiale.