Hierarchic normal forms for desynchronization


Jean-Pierre Talpin, Albert Benveniste, Benoît Caillaud and Paul Le Guernic

We present an in-depth discussion of the relationships between synchrony and asynchrony. Simple models of both paradigms are presented, and we state theorems which guarantee correctdesynchronization, meaning that the original synchronous semantics can be reconstructed from the result of this desynchronization. This theory can be used as a basis for correct distributed code generation. The present paper presents a new data structure, the hierarchic normal form (HNF) for a transition relation, which is instrumental in implementing this theory. HNFdiffer from Bdd's. They are canonical and do not need prior ordering of the variables for this. They reveal clock hierarchies as well as nested states such as exhibited in Statecharts. They are the adequate data structures to implement correct desynchronization. They can be seen as a systematic calculus of don't care in hardware design, and play a central role in optimizations for code generation. We provide compositional algorithms for computing HNF. We illustrate this on a Statecharts example. The whole approach is implemented in the Signal compiler.
 

Keywords : synchronous languages, desynchronization, distribution.
 
 

  gzippped postscript