Synthèse de contrôleurs séquentiels QDI faible consommation prouvés corrects

ISBN : 978-2-84813-155-9The study of asynchronous circuits is an area where much research has been conducted in recent years. Asynchronous circuits have shown several interesting features like robustness, scalability, low consumption or low electromagnetic radiation. Among the different classes of asynchronous circuits, Quasi Delay Insensitive circuits (QDI) showed very interesting characteristics in terms of low power consumption and robustness to variations of PVT (Process, Voltage, and Temperature). The use of these circuits is particularly well suited for applications operating in a critical environment and for which consumption is paramount. In this framework, the work of this thesis aims the low power consumption design and synthesis of asynchronous state machines (QDI). A method for synthesizing low-consumption asynchronous sequential controllers has been developed. The method relies on an adequate modeling of controllers and a direct mapping synthesis technique using specific components called sequencers. This technique is suitable for synthesizing large controllers. The circuits obtained are formally verified to ensure their properties in terms of robustness and are proved functionally correct. Thereby, a formal verification method has been implemented to validate the sequential controllers on the one hand, and more generally, any other asynchronous circuit. This technique uses a hierarchical model of asynchronous circuits in PSL and a formal verification tool called RAT.L'étude des circuits asynchrones est un secteur dans lequel de nombreuses recherches ont été effectuées ces dernières années. Les circuits asynchrones ont démontré plusieurs caractéristiques intéressantes comme la robustesse, l'extensibilité, la faible consommation ou le faible rayonnement électromagnétique. Parmi les différentes classes de circuits asynchrones, les circuits quasi-insensibles aux délais (QDI) ont montré des caractéristiques extrêmement intéressantes en termes de faible consommation et de robustesse aux variations PVT (Process, Voltage, Temperature). L'usage de ces circuits est notamment bien adapté aux applications fonctionnant dans un environnement sévère et pour lesquelles la consommation est un critère primordial. Les travaux de cette thèse s'inscrivent dans ce cadre et visent la conception et la synthèse de machines à états asynchrones (QDI) faiblement consommantes. Une méthode de synthèse dédiée à des contrôleurs asynchrones à faible consommation a donc été développée. Cette technique s'est montrée particulièrement efficace pour synthétiser les contrôleurs de grande taille. La méthode s'appuie sur une modélisation appropriée des contrôleurs et une technique de synthèse dirigée par la syntaxe utilisant des composants spécifiques appelés séquenceurs. Les circuits obtenus ont été vérifiés formellement afin de s'assurer de leurs propriétés en termes de robustesse et de correction fonctionnelle. A cette occasion, une méthode de vérification formelle a été mise en place pour valider les contrôleurs d'une part, et plus généralement, n'importe quel circuit asynchrone d'autre part. Cette technique fait appel à une modélisation hiérarchique des circuits asynchrones en PSL et à un outil de vérification formelle (RAT)