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

From bibtex.

Abstract

The 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.