From clock-driven to data-driven models

Clock/time-driven models are powerful abstractions of real-time systems, as e.g., provided by the synchronous models of computation which lend themselves well for simulation and verification. At every clock cycle, new inputs are read, computations are performed in zero-time, and results are immediately/synchronously communicated between components. However, such zero-time idealizations are not realistic since computation and communication finally takes time in implementations. For implementations, data-driven execution models have the advantage to impose no timing constraints other than arrival of input data, and thus, these models are perfectly suited for distributed or other kinds of asynchronous implementations. For this reason, modern model-based design flows consider the desynchronization of synchronous models for system synthesis which is possible for the subclass of endochronous systems only. While definitions of endochrony were considered for years, it is shown in this paper how to efficiently verify endochrony by SAT solving. Our procedure consists of two steps: In the first step, we introduce buffers to the interface of a clock-driven component, so that its inputs can arrive at different points of time. After this step, clocks of signals are viewed as `instructions´ telling the component which input values have to be consumed for the current reaction.We call such components clock-scheduled. In the second step, we remove the clocks from the interface of the clock-scheduled components, so that the component may now become nondeterministic. We prove in this paper that a synchronous component is endochronous, if and only if the clock signals can be safely removed in this step without destroying determinism. Based on this result, we present a decision procedure based on symbolic system representations to check whether components are endochronous. Preliminary experimental results show the effectiveness of our method.