Les travaux présentés dans cette thèse visent à produire automatiquement des prototypes de circuits de communication et de contrôle à partir de spécifications temporelles déclaratives. Partant d'un ensemble de propriétés écrites en langage PSL, nous produisons un modèle RTL synthétisable automatiquement. La méthode proposée est modulaire, contrairement aux méthodes publiées antérieurement qui étaient fondées sur la théorie des automates. Pour chaque propriété, nous produisons un composant qui observe certains opérandes et génère des chronogrammes pour les autres opérandes : le module réactif. Tout d'abord, une bibliothèque des modules réactifs primitifs a été développée pour les opérateurs FL et SERE. Pour ce faire, une relation de dépendance a été définie pour chaque opérateur : fondée sur la sémantique de l'opérateur, elle exprime la dépendance entre ses opérandes. Ensuite, la relation de dépendance de chaque opérateur est interprétée comme un composant matériel qui met en œuvre l'opérateur : c'est le module réactif primitif de l'opérateur. À l'aide de cette formalisation, nous proposons une méthode pour déterminer automatiquement quels signaux d'une propriété sont observés et lesquels sont générés. Dans le cas où il n'est pas possible de déterminer le sens du signal, un solveur est ajouté pour identifier la valeur du signal. Le solveur sert aussi à déterminer la valeur d'un signal généré par plusieurs propriétés. Le circuit final est l'interconnexion des modules réactifs et des solveurs pour l'ensemble des propriétés. Un outil prototype, SyntHorus2, qui est une extension d'HORUS, a été mis développé. Il prend les propriétés PSL comme entrées et génère le code VHDL synthétisable du circuit. En outre, il génère des propriétés complémentaires pour vérifier si l'ensemble des spécifications est cohérent et complet. La méthode est efficace et synthétise des circuits de commande en quelques secondes. Les résultats que nous avons obtenus sur des jeux d'essais classiques montrent que notre technique compile les propriétés plus efficacement que les outils prototypes qui l'ont précédée. / The work presented in this thesis aims at automatically prototype communication and control designs from declarative temporal specifications. From a set of PSL properties, we produce a synthesizable RTL design automatically. The proposed method is modular, in contrast to previously published methods that were based on automata theory. From each property, we produce a component that observes some operands and generates waveforms for the other operands: the reactant. First, a library of primitive reactants has been provided for FL and SERE operators. To this goal, a dependency relation is defined for each operator that expresses the dependency among its operands using the operator's semantics. Then, the dependency relation of each operator is interpreted as a hardware component that implements the operator: the operator's primitive reactant. Using this formalization, a method is proposed to automatically decide which signals of a property are observed and which are generated. In the cases when specifying the signal direction is not possible, a solver is implemented to identify the signal value. In addition, the way of identifying the value of the signal that is generated in several properties is addressed. The final circuit is the interconnection of the properties' reactants and solvers. A prototype tool SyntHorus2, which is an extension to HORUS, has been developed. It takes PSL properties as its inputs, and generates the synthesizable VHDL code of the circuit. In addition, it generates some complementary properties to verify if the set of specification is coherent and complete. The method is efficient, and synthesizes control circuits in a few seconds. Results obtained on classical benchmarks show that our technique compiles properties more efficiently than previous prototype tools.

Soft multiprocessor systems exploit the plentiful computational resources available in field programmable devices. By virtue of their adaptability and ability to support coarse grained parallelism, they serve as excellent platforms for rapid prototyping and design space exploration of embedded multiprocessor applications. As complex applications emerge, careful mapping, processor and interconnect customization are critical to the overall performance of the multiprocessor system. In this thesis, we have developed an automated scalable framework to efficiently map applications written in a high-level programmer-friendly language to customizable soft-cores. The framework allows the user to specify the application in a high-level language called Streamit. After an initial analysis of the application, a soft multiprocessor system is generated automatically using a set of customizable SPREE processors which communicate with each other over point-to-point FIFO connections. Several micro-architectural features of the processors are then automatically customized on a per-application basis to improve system area, performance and power consumption. The efficiency and scalability of this approach has been validated using a diverse set of eight audio, video and signal processing benchmarks on soft multiprocessor systems consisting of one to sixteen processors. Results show that generated soft multiprocessor systems consisting of sixteen processors can offer up to 6x speedup over a conventional single processor system. Our experiments with soft multiprocessor interconnection networks show that point-to-point topologies perform approximately 2x better than mesh topologies. Finally, we demonstrate that application-specific customizations on the instruction set, memory size, and inter-processor buffer size can improve the area and performance of the generated soft multiprocessor systems. The developed framework facilitates rapid design space exploration of soft multiprocessors.

Embedded Systems may have competing design objectives, such as to maximize the reliability, increase the functional safety, minimize the product cost, and minimize the energy consumption. The architectures must be therefore configured to meet varied requirements and multiple design objectives. In particular, reliability and safety are receiving increasing attention. Consequently, the configuration of fault-tolerant mechanisms is a critical design decision. This work proposes a method for automatic selection of appropriate fault-tolerant design patterns, optimizing simultaneously multiple objective functions. Firstly, we present an exact method that leverages the power of Satisfiability Modulo Theory to encode the problem with a symbolic technique. It is based on a novel assessment of reliability which is part of the evaluation of alternative designs. Afterwards, we empirically evaluate the performance of a near-optimal approximation variation that allows us to solve the problem even when the instance size makes it intractable in terms of computing resources. The efficiency and scalability of this method is validated with a series of experiments of different sizes and characteristics, and by comparing it with existing methods on a test problem that is widely used in the reliability optimization literature.

Systems populating the Ubiquitous Computing environment are characterized by an often extreme level of heterogeneity at different layers which prevents their seamless interoperability. In this environment, heterogeneous protocols would cooperate to reach some common goal even though they meet dynamically and do not have a priori knowledge of each other. Although numerous efforts have been done in the literature, the automated and run-time interoperability is still an open challenge for such environment. Therefore, this thesis focuses on overcoming the interoperability problem between heterogeneous protocols in the Ubiquitous Computing. In particular, we aim at providing a means to drop the interoperability barriers by automatically eliciting a way for the protocols to interact. The solution we propose is the automated synthesis of emerging mediating connectors (also called mediators or connectors). Specifically, we concentrate our efforts to: (i) devising AMAzING, a process to synthesize mediators, (ii) characterizing protocol mismatches and related mediator patterns, and (iii) designing MediatorS, a theory of mediating connectors. The theory, and the process, are put in practice by applying them to a real world application, and have been adopted by the European Research Project CONNECT.