Removing causality cycle of synchronous programs with sequential data-flow recursion

Synchronous language has being fashioned in applications with high safety criticality such as aviation electronics. However, the synchronous programming paradigm challenges compiler design because of its micro-step execution in zero time. This can yield causality cycles that must be resolved to generate single-threaded code. The existing methods donpsilat take next tick operation introduced recently in synchronous languages into account. In this paper, we indicate that removal of causality cycles of programs with next tick operation can be performed by two fixed-points computations, one for the initialized data-flow and another for the transited data-flow. Moreover, we elaborate on an implementation based on binary decision diagrams (BDDs). At the same time, we also provide constructive semantic interpretation for our dual rails encoding mechanism.