The research reported in this dissertation is motivated by two trends in the system-on-chip (SoC) design industry. First, due to the incessant technology scaling, the interconnect delays are getting larger compared to gate delays, leading to multi-cycle delays in communication between functional blocks on the chip, which makes implementing a synchronous global clock difficult, and power consuming. As a result, globally asynchronous and locally synchronous (GALS) designs have been proposed for future SoCs. Second, due to time-to-market pressure, and productivity gain, intellectual property (IP) block reuse is a rising trend in SoC design industry. Predesigned IPs may already be optimized and verified for timing for certain clock frequency, and hence when used in an SoC, GALS offers a good solution that avoids reoptimizing or redesigning the existing IPs. A special case of GALS, known as Latency-Insensitive Protocol (LIP) lets designers adopt the well-understood and developed design flow of synchronous design while solving the multi-cycle latency at the interconnects. The communication fabrics for LIP are synchronous pipelines with hand shaking. However, handshake based protocol has complex control logics and the unnecessary handshake brings down the system's throughput. That is why scheduling based LIP was proposed to avoid the hand-shakes by pre-calculated clock gating sequences for each block. It is shown to have better throughput and easier to implement. Unfortunately, static scheduling only exists for bounded systems. Therefore, this type of design in literatures restrict their discussions to systems whose graphic representation has a single strongly connected component (SCC), which by the theory is bounded. This dissertation provides an optimization design flow for LIP synthesis with respect to back pressure, throughput and buffer sizes. This is based on extending the scheduled LIP with minimum modifications to render it general enough to be applicable to most systems, especially those with multiple SCCs. In order to guarantee the design correctness, a formal framework that can analyze concurrency and prevent fallacious behaviors such as overflow, deadlock etc., is required. Among many formal models of concurrency used previously in asynchronous system design, marked graphs, periodic clock calculus and polychrony are chosen for the purpose of modeling, analyzing and verifying in this work. Polychrony, originally developed for embedded software modeling and synthesis, is able to specify multi-rate interfaces. Then a synchronous composition can be analyzed to avoid incompatibly and combinational loops which causes incorrect GALS distribution. The marked graph model is a good candidate to represent the interconnection network which is quite suitable for modeling the communication and synchronizations in LIP. The periodic clock calculus is useful in analyzing clock gating sequences because periodic clock calculus easily captures data dependencies, throughput constraints as well as buffer sizes required for synchronization. These formal methods help establish a formally based design flow for creating a synchronous design and then transforming it into a GALS implementation either using LIP or in a more general GALS mechanisms. / Ph. D.

Au cours des dernières décennies, la complexité croissante des systèmes de production et de leur commande a rendu crucial le besoin d’utiliser les méthodes formelles pour faire face aux problèmes relatifs au contrôle, à la fiabilité, au diagnostic des fautes et à l’utilisation optimale des ressources dans les installations de production. Cela concerne en particulier les systèmes automatisés de production (SAP), caractérisés par des cycles technologiques complexes qui doivent s’adapter à des conditions changeantes. Les SAP modernes sont des sous-systèmes interconnectés tels que des machines à commande numérique, des stations d'assemblage , des véhicules guidés automatisés (AGV), des cellules robotisées, des convoyeurs et des systèmes de contrôle par ordinateur. Les fabricants utilisent des machines automatisées et des contrôleurs pour assurer des produits de qualité plus rapidement et plus efficacement. Aussi, ces systèmes automatisés peuvent fournir des informations essentielles pour aider les gestionnaires à prendre les bonnes décisions. Cependant, en raison de la grande flexibilité des SAP, des défaillances telles qu’un mauvais assemblage ou le dépôt d’une pièce dans un tampon inapproprié peuvent se produire lors du fonctionnement du système. De tels dysfonctionnements diminuent la productivité du système générant ainsi des pertes économiques et des effets perturbateurs sur le système. En conséquence, le problème de l’optimisation des performances des SAP est impératif.Cette thèse se focalise sur l’évaluation et l’optimisation des performances des systèmes de production automatisés via le modèle des réseaux de Pétri temporisés. / In the last decades, there has been a constant increase in the awareness of company management about the importance of formal techniques in industrial settings to address problems related to monitoring and reliability, fault diagnosis, and optimal use of resources, during the management of plants. Of particular relevance in this setting are the so-called Automated Manufacturing Systems (AMSs), which are characterized by complex technological cycles that must adapt to changing demands. Modern AMSs are interconnected subsystems such as numerically controlled machines, assembly stations, automated guided vehicles, robots, conveyors and computer control systems. Manufacturers are using automated machines and controls to produce quality products faster and more efficiently. Meanwhile, these automated systems can provide critical information to help managers make good business decisions. However, due to the high flexibility of AMSs, failures such as a wrong assembly or a part put in a wrong buffer may happen during the operation of the system. Such failures may decrease the productivity of the system which has an economical consequence and can cause a series of disturbing issues. As a result, the performance optimization in AMSs are imperative. This thesis focuses on the performance evaluation and performance optimization of automated manufacturing systems using timed Petri nets models.