No description available.

No description available.

No description available.

No description available.

No description available.

No description available.

We present a generic proof methodology to automatically prove correctness of design transformations introduced at the Register-Transfer Level (RTL) to achieve lower power dissipation in hardware systems. We also introduce a new algorithm to reduce switching activity power dissipation in microprocessors. We further apply our technique in a completely different domain of dynamic power management of Systems-on-Chip (SoCs). We demonstrate our methodology on real-life circuits. In this thesis, we address the dual problem of transforming hardware systems at higher levels of abstraction to achieve lower power dissipation, and a reliable way to verify the correctness of the afore-mentioned transformations. The thesis is in three parts. The first part introduces Instruction-driven Slicing, a new algorithm to automatically introduce RTL/System level annotations in microprocessors to achieve lower switching power dissipation. The second part introduces Dedicated Rewriting, a rewriting based generic proof methodology to automatically prove correctness of such high-level transformations for lowering power dissipation. The third part implements dedicated rewriting in the context of dynamically managing power dissipation of mobile and hand-held devices. We first present instruction-driven slicing, a new technique for annotating microprocessor descriptions at the Register Transfer Level in order to achieve lower power dissipation. Our technique automatically annotates existing RTL code to optimize the circuit for lowering power dissipated by switching activity. Our technique can be applied at the architectural level as well, achieving similar power gains. We first demonstrate our technique on architectural and RTL models of a 32-bit OpenRISC pipelined processor (OR1200), showing power gains for the SPEC2000 benchmarks. These annotations achieve reduction in power dissipation by changing the logic of the design. We further extend our technique to an out-of-order superscalar core and demonstrate power gains for the same SPEC2000 benchmarks on architectural and RTL models of PUMA, a fixed point out-of-order PowerPC microprocessor. We next present dedicated rewriting, a novel technique to automatically prove the correctness of low power transformations in hardware systems described at the Register Transfer Level. We guarantee the correctness of any low power transformation by providing a functional equivalence proof of the hardware design before and after the transformation. Dedicated rewriting is a highly automated deductive verification technique specially honed for proving correctness of low power transformations. We provide a notion of equivalence and establish the equivalence proof within our dedicated rewriting system. We demonstrate our technique on a non-trivial case study. We show equivalence of a Verilog RTL implementation of a Viterbi decoder, a component of the DRM System-On-Chip (SoC), before and after the application of multiple low power transformations. We next apply dedicated rewriting to a broader context of holistic power management of SoCs. This in turn creates a self-checking system and will automatically flag conflicting constraints or rules. Our system will manage power constraint rules using dedicated rewriting specially honed for dynamic power management of SoC designs. Together, this provides a common platform and representation to seamlessly cooperate between hardware and software constraints to achieve maximum platform power optimization dynamically during execution. We demonstrate our technique in multiple contexts on an SoC design of the state-of-the-art next generation Intel smartphone platform. Finally, we give a proof of instruction-driven slicing. We first prove that the annotations automatically introduced in the OR1200 processor preserve the original functionality of the machine using the ACL2 theorem prover. Then we establish the same proof within our dedicated rewriting system, and discuss the merits of such a technique and a framework. In the context of today's shrinking hardware and mobile internet devices, lowering power dissipation is a key problem. Verifying the correctness of transformations which achieve that is usually a time-consuming affair. Automatic and reliable methods of verification that are easy to use are extremely important. In this thesis we have presented one such transformation, and a generic framework to prove correctness of that and similar transformations. Our methodology is constructed in a manner that easily and seamlessly fits into the design cycle of creating complicated hardware systems. Our technique is also general enough to be applied in a completely different context of dynamic power management of mobile and hand-held devices. / text

Dieser Bericht präsentiert RACR-NET, eine Schnittstelle der Referenzattributgrammatik-gesteuerten Graphersetzungsbibliothek RACR für C#. RACR-NET ermöglicht die Nutzung der deklarativen, dynamischen Sprachspezifikations-, Instanziierungs- und Auswertungsmeachanismen der RACR Scheme-Bibliothek in der objektorientierten Programmierung. Dies umfasst insbesondere die automatische inkrementelle Auswertung attributbasierter semantischer Analysen und somit das automatische Cachen parametrisierter Funktionsmethoden. Graphersetzungen entsprechen hierbei Zustandsänderungen von Objektinstanzen und der Invalidierung abgeleiteter Berechnungen. Schwerpunkt dieses Berichts ist die objektorientierte Programmierschnittstelle von RACR-NET, dessen praktische Anwendung und Implementierung. Der Bericht ist ein Referenzhandbuch für RACR-NET Anwender und Entwickler.

Cette thèse traite de la conception de méthodes automatisées ou semi-automatisées pour détecter et identifier des algorithmes cryptographiques dans des programmes compilés en langage machine. La première méthode proposée a pour but l'identification de primitives symétriques. L'implémentation en langage machine d'une primitive symétrique, assimilée à une suite d'instructions, est représentée par un graphe. Sous cette forme, le code est modifié à l'aide de règles de réécriture tout en préservant une certaine notion de sémantique lors d'une phase dite de normalisation. L'objectif est de faire émerger des expressions communes à différentes implémentations d'une même primitive. Ces expressions servent alors de base à la création de signatures efficaces. La recherche de ces signatures s'effectue à l'aide d'un algorithme énumérant les isomorphismes de sous-graphe. La seconde méthode, conçue en complément de la première, produit une représentation synthétique facilitant l'identification des modes opératoires. Cette représentation se définit comme le plus petit sous-graphe préservant les distances entre des sous-ensembles de nœuds précédemment identifiés comme étant les paramètres d'entrée et de sortie des primitives impliquées. / This thesis is about the design of automatic or semi-automatic methods to detect and identify cryptographic algorithms inside programs compiled into machine code. Two methods are presented. The objective of the first method is to identify cryptographic primitives. A machine code implementation of a cryptographic primitive, regarded as a sequence of instructions, is represented by a graph structure. During a normalization phase, a set of rewrite rules is used to modify this graph representation while preserving a specific notion of semantics. The goal is to converge towards expressions which are shared across several implementations of the same primitive. We use these expressions as a basis to create efficient signatures. A subgraph isomorphism enumeration algorithm is used to search for signatures. The second method is built on top of the first one. It produces a synthetic representation designed to help in the identification of modes of operation. This synthetic representation is defined as the smallest subgraph which preserve distances between sets of vertices previously identified as the input and output parameters of the primitives involved within the mode of operation.

This report presents RACR, a reference attribute grammar library for the programming language Scheme. RACR supports incremental attribute evaluation in the presence of abstract syntax tree rewrites. It provides a set of functions that can be used to specify abstract syntax tree schemes and their attribution and construct respective trees, query their attributes and node information and annotate and rewrite them. Thereby, both, reference attribute grammars and rewriting, are seamlessly integrated, such that rewrites can reuse attributes and attribute values change depending on performed rewrites – a technique we call Reference Attribute Grammar Controlled Rewriting. To reevaluate attributes influenced by abstract syntax tree rewrites, a demand-driven, incremental evaluation strategy, which incorporates the actual execution paths selected at runtime for control-flows within attribute equations, is used. To realize this strategy, a dynamic attribute dependency graph is constructed throughout attribute evaluation – a technique we call Dynamic Attribute Dependency Analyses. The report illustrates RACR's motivation, features, instantiation and usage. In particular its application programming interface is documented and exemplified. The report is a reference manual for RACR developers. Further, it presents RACR’s complete implementation and therefore provides a good foundation for readers interested into the details of reference attribute grammar controlled rewriting and dynamic attribute dependency analyses.