Résumé
Polychronous specifications express concurrent, multi-clocked models which capture multiple threads of computation operating relatively asynchronous to each other. A clock of a variable in this context, is the totally ordered set of instants at which events occur on that variables. However, the notion of instant here is logical as opposed to real-time instants. The instants of different clocks may be partially ordered. The executable code synthesis from Polychronous specifications relies on computation of schedules through clock calculus. Unfortunately, it is often hard to distinguish from true causal loops which cause deadlocks from apparent causal loops which do not. The SIGNAL compiler in the Polychrony tool-set currently rejects all programs with apparent causal loops, thus rejecting a large set of valid specifications. A recently developed polychronous formalism MRICDF and its tool-set EmCodeSyn do the same. Even in the Polychrony literature, the deadlock causing loop detection based on Boolean satisfiability is not enough to discern all possible false loops, thereby still rejecting a lot of valid specifications. In order to not reject programs whose apparent loops are never realizable, a theory of reals or integers or other data types are required. In this paper, we formulate the detection of false loops in MRICDF as a decision problem in Satisfiability Modulo Theory (SMT). Due to recent interests in SMT solvers, a number of efficient solvers are available which offer a greater expressiveness in dealing with non Boolean constraints and allow us to discern false loops from realizable causalities in reasonable computation time. This paper proposes an SMT based synthesis technique which demonstrates that several polychronous specifications rejected by the Polychrony/EmCodeSyn synthesis tools due to their inability to identify only true causal loops, can be synthesized as correct sequential embedded software.