Nous présentons une nouvelle approche pour formuler et calculer le temps de séparation
des événements utilisé dans l’analyse et la vérification de différents systèmes cycliques et
acycliques sous des contraintes linéaires-min-max avec des composants ayant des délais finis et
infinis. Notre approche consiste à formuler le problème sous la forme d’un programme entier
mixte, puis à utiliser le solveur Cplex pour avoir les temps de séparation entre les événements.
Afin de démontrer l’utilité en pratique de notre approche, nous l’avons utilisée pour la
vérification et l’analyse d’une puce asynchrone d’Intel de calcul d’équations différentielles.
Comparée aux travaux précédents, notre approche est basée sur une formulation exacte et elle
permet non seulement de calculer le maximum de séparation, mais aussi de trouver un
ordonnancement cyclique et de calculer les temps de séparation correspondant aux différentes
périodes possibles de cet ordonnancement.
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 the solver Cplex 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 based on exact formulation and it allows not only
the maximum separation computing, but it can also provide cyclic schedules and compute bound
on possible periods of such schedules.
