Timing verification of cyclic systems based on temporal constraint analysis

We present a new approach for formulating and computing time separation of events used for timing analysis of different types of cyclic and acyclic systems that obey to linear-min-max type constraints with finite and infinite bounded component delays. Our approach consists of formulating the problem as a mixed integer program then using a branch and cut algorithm implemented within a solver to get time separations between events. In order to demonstrate the practical use of our approach we apply it for the verification and analysis of an Intel asynchronous differential equation solver chip. Compared to previous work, our approach is exact while remaining efficient. It allows not only the maximum separation computing but can also provide cyclic schedules and compute bound on possible periods of such schedules.