According to Moore's law, Integrated Chips (IC) doubles its capacity every 18 months. This causes an exponential increase of the available area, and hence,the complexity of modern digital designs. This consistent enormous gross challenges different research areas in Electronic Design Automation (EDA). Thus, various EDA applications such as equivalence checking, model checking, Automatic Test Pattern Generation (ATPG), functional Bi-decomposition, and technology mapping need to keep pace with these challenges. In this thesis, we are concerned with improving the quality and performance of different EDA algorithms particularly in area of hardware verification and synthesis. First, we introduce algorithms to manipulate Reduced Ordered Binary Decision Diagrams (ROBDD) on multi-core machines. In order to perform multiple BDD operations concurrently, our algorithm uses a breadth-first search (BFS). As ROBDD algorithms are memory-intensive, maintaining locality of data is an important issue. Therefore, we propose the usage of Hopscotch hashing technique for both Unique Table and BFS Queues to improve the construction time of ROBDD on the parallel platform. Hopscotch hashing technique not only improves the locality of the manipulating data, but also provides a way to cache recently performed BDD operation. Consequently, The time and space usage can be traded off. Secondly, we used static implications to enhance the performance of SAT-based Bounded Model Checking (BMC) problem. we propose a parallel deduction engine to efficiently utilize low-cost off-shelf multi-core processors to compute the implications. With this engine, we can significantly reduce the computational processing time in analyzing the deduced implications. Secondly, we formulate the clause filter problem as an elegant set-covering problem. Thirdly, we propose a novel greedy algorithm based on the Johnson's algorithm to find the optimal set of clauses that would accelerate BMC solution. Thirdly, we proposed a novel synthesis paradigm to achieve timing-closure called Timing-Aware CUt Enumeration (TACUE). In TACUE, optimization is conducted through three aspects: First, we propose a new divide-and-conquer strategy that generates multiple sub-cuts on the critical parts of the circuit. Secondly, cut enumeration have been applied in two cutting strategies. In the topology-aware cutting strategy, we preserve the general topology of the circuit by applying TACUE in only self-contained cuts. Meanwhile, the topology-masking cutting strategy investigates circuit cuts beyond their current topology. Thirdly, we proposed an efficient parallel synthesis framework to reduce computation time for synthesizing TACUE sub-cuts. We conducted experiments on large and difficult industrial benchmarks. Finally, we proposed the first scalable SAT-based approaches for Observability Dont Care (ODC) clock gating. Moreover we intelligently choose those inductive invariants candidates such that their validation will benefit the purpose in clock-gating-based low-power design. / Ph. D.

Seit langem ist die Intelligenz des Menschen für viele Forscher und Philosophen ein faszinierendes Forschungsobjekt. Mit dem Aufkommen der Computertechnik erscheint nun zum ersten mal der Traum, einige dieser typisch menschlichen Fähigkeiten nicht nur zu verstehen, sondern nachbauen oder in Teilgebieten gar übertreffen zu können, als realistisch. Ein wichtiger Teil dieses mit "Künstliche Intelligenz" überschriebenen Forschungsgebietes ist das Schließen über Aktionen und Veränderung. Hier wird versucht, die menschliche Fähigkeit, die Effekte seiner Aktionen vorauszusehen und Pläne zum Erreichen von Zielen zu schmieden, nachzubilden. Ein aktives Forschungsgebiet in diesem Rahmen ist der Fluentkalkül, ein Formalismus zur Modellierung von Aktionen und Veränderung. Er stellt Mittel bereit, in der ein automatischer Agent seine Umgebung und die Effekte seiner Aktionen im Rahmen der mathematischen Logik darstellen kann, um mit Hilfe von logischem Schließen sein Verhalten zu planen. Obwohl zum Fluentkalkül viele Arbeiten existieren, die dessen Anwendungsbereiche und Semantik erweitern, gibt es doch noch relativ wenige Arbeiten zum effizienten Schlussfolgern. Dies ist ein Hauptaugenmerk der vorliegenden Arbeit. Es wird ein Algorithmus geschaffen, der Erkenntnisse aus effizienten Verfahren zum Modelchecking mit Binären Entscheidungsdiagrammen (BDDs) sinngemäß überträgt und für ein Fragment des Fluentkalkül erweitert. Damit können nun auch Planungsprobleme von Fluentkalkül-Planern gelöst werden, die der realisierten symbolischen Breitensuche besser zugänglich sind, als der bisher aussschliesslich verwendeten heuristischen Tiefensuche. Um eine leichtere Vergleichbarkeit Fluentkalkül-basierter Planungsverfahren mit anderen Planungsalgorithmen zu ermöglichen, wurde eine Übersetzung des ADL-Fragments der Planungsdomänenbeschreibungssprache PDDL in den Fluentkalkül geschaffen. Damit können zahlreiche Planungsprobleme aus der Literatur und Planungsdomänenbibliotheken auch mit Fluentkalkül-Planern bearbeitet werden. Die Übersetzung kann zugleich als formale Semantik des nur informal spezifizierten PDDL dienen.

Os ROBDDs são estruturas utilizadas com sucesso em ferramentas de CAD para microeletrônica. Estas estruturas permitem a representação canônica de funções booleanas ao se estabelecer um ordenamento fixo de variáveis. No contexto de um gerador automático de células lógicas para circuitos integrados, os ROBDDs podem servir de base para a derivação de redes de transistores cujo comportamento elétrico equivale ao comportamento lógico de uma função booleana desejada. Nas redes de transistores derivadas de ROBDDs, o posicionamento relativo dos transistores é determinado pelo ordenamento de variáveis. O efeito do reordenamento de transistores já foi estudado na década de noventa e sabe-se de sua influência sobre características de área, atraso e potência de um circuito digital. Entretanto, estes estudos limitam-se à topologia CMOS complementar série/paralelo, que é a topologia de redes de transistores mais comum. Neste trabalho, explora-se o efeito do reordenamento de variáveis nas características de área e atraso de circuitos mapeados com seis famílias lógicas diferentes, cujas células constituem redes de transistores derivadas de ROBDDs. Em geral, os resultados dos experimentos indicam que, para estas famílias lógicas, selecionar ordenamentos, onde transistores controlados por sinais mais críticos posicionam-se relativamente mais próximos à saída da célula, pode levar ao mapeamento de circuitos com atraso 16,4% inferior, em média, ao atraso do circuito equivalente com ordenamentos selecionados para obtenção da menor área possível e ignorando-se os atrasos de chegada nas entradas de uma célula. / The ROBDDs are structures that have been successfully used in CAD tools for microelectronics. These structures allow canonical representation of boolean functions when established a fixed variable ordering. In the context of an automatic logic cell generator for integrated circuits, ROBDDs may serve as a base for deriving transistor networks from which electrical behavior is equivalent to the logic behavior of a specified boolean function. With ROBDD derived transistor networks, the relative placement of transistors is determined by variable ordering. The effect of transistor reordering was already studied in the nineties and we know about its influence over area, delay and power characteristics of an integrated circuit. However, these studies were limited to complementary series/parallel CMOS topology, which is the standard for transistor networks topology. In this work, the effect of variable reordering is explored over area and delay characteristics of circuits mapped to six different logic families, where cells are designed with ROBDD derived transistor networks. Experimental results indicate that, in general, placing transistors controlled by the most critical signals closer to cell output may lead to a circuit mapping with an average 16.4% less delay than an equivalent circuit where orderings for smallest possible area are selected and input arrival times of a cell are ignored.

Os ROBDDs são estruturas utilizadas com sucesso em ferramentas de CAD para microeletrônica. Estas estruturas permitem a representação canônica de funções booleanas ao se estabelecer um ordenamento fixo de variáveis. No contexto de um gerador automático de células lógicas para circuitos integrados, os ROBDDs podem servir de base para a derivação de redes de transistores cujo comportamento elétrico equivale ao comportamento lógico de uma função booleana desejada. Nas redes de transistores derivadas de ROBDDs, o posicionamento relativo dos transistores é determinado pelo ordenamento de variáveis. O efeito do reordenamento de transistores já foi estudado na década de noventa e sabe-se de sua influência sobre características de área, atraso e potência de um circuito digital. Entretanto, estes estudos limitam-se à topologia CMOS complementar série/paralelo, que é a topologia de redes de transistores mais comum. Neste trabalho, explora-se o efeito do reordenamento de variáveis nas características de área e atraso de circuitos mapeados com seis famílias lógicas diferentes, cujas células constituem redes de transistores derivadas de ROBDDs. Em geral, os resultados dos experimentos indicam que, para estas famílias lógicas, selecionar ordenamentos, onde transistores controlados por sinais mais críticos posicionam-se relativamente mais próximos à saída da célula, pode levar ao mapeamento de circuitos com atraso 16,4% inferior, em média, ao atraso do circuito equivalente com ordenamentos selecionados para obtenção da menor área possível e ignorando-se os atrasos de chegada nas entradas de uma célula. / The ROBDDs are structures that have been successfully used in CAD tools for microelectronics. These structures allow canonical representation of boolean functions when established a fixed variable ordering. In the context of an automatic logic cell generator for integrated circuits, ROBDDs may serve as a base for deriving transistor networks from which electrical behavior is equivalent to the logic behavior of a specified boolean function. With ROBDD derived transistor networks, the relative placement of transistors is determined by variable ordering. The effect of transistor reordering was already studied in the nineties and we know about its influence over area, delay and power characteristics of an integrated circuit. However, these studies were limited to complementary series/parallel CMOS topology, which is the standard for transistor networks topology. In this work, the effect of variable reordering is explored over area and delay characteristics of circuits mapped to six different logic families, where cells are designed with ROBDD derived transistor networks. Experimental results indicate that, in general, placing transistors controlled by the most critical signals closer to cell output may lead to a circuit mapping with an average 16.4% less delay than an equivalent circuit where orderings for smallest possible area are selected and input arrival times of a cell are ignored.

Os ROBDDs são estruturas utilizadas com sucesso em ferramentas de CAD para microeletrônica. Estas estruturas permitem a representação canônica de funções booleanas ao se estabelecer um ordenamento fixo de variáveis. No contexto de um gerador automático de células lógicas para circuitos integrados, os ROBDDs podem servir de base para a derivação de redes de transistores cujo comportamento elétrico equivale ao comportamento lógico de uma função booleana desejada. Nas redes de transistores derivadas de ROBDDs, o posicionamento relativo dos transistores é determinado pelo ordenamento de variáveis. O efeito do reordenamento de transistores já foi estudado na década de noventa e sabe-se de sua influência sobre características de área, atraso e potência de um circuito digital. Entretanto, estes estudos limitam-se à topologia CMOS complementar série/paralelo, que é a topologia de redes de transistores mais comum. Neste trabalho, explora-se o efeito do reordenamento de variáveis nas características de área e atraso de circuitos mapeados com seis famílias lógicas diferentes, cujas células constituem redes de transistores derivadas de ROBDDs. Em geral, os resultados dos experimentos indicam que, para estas famílias lógicas, selecionar ordenamentos, onde transistores controlados por sinais mais críticos posicionam-se relativamente mais próximos à saída da célula, pode levar ao mapeamento de circuitos com atraso 16,4% inferior, em média, ao atraso do circuito equivalente com ordenamentos selecionados para obtenção da menor área possível e ignorando-se os atrasos de chegada nas entradas de uma célula. / The ROBDDs are structures that have been successfully used in CAD tools for microelectronics. These structures allow canonical representation of boolean functions when established a fixed variable ordering. In the context of an automatic logic cell generator for integrated circuits, ROBDDs may serve as a base for deriving transistor networks from which electrical behavior is equivalent to the logic behavior of a specified boolean function. With ROBDD derived transistor networks, the relative placement of transistors is determined by variable ordering. The effect of transistor reordering was already studied in the nineties and we know about its influence over area, delay and power characteristics of an integrated circuit. However, these studies were limited to complementary series/parallel CMOS topology, which is the standard for transistor networks topology. In this work, the effect of variable reordering is explored over area and delay characteristics of circuits mapped to six different logic families, where cells are designed with ROBDD derived transistor networks. Experimental results indicate that, in general, placing transistors controlled by the most critical signals closer to cell output may lead to a circuit mapping with an average 16.4% less delay than an equivalent circuit where orderings for smallest possible area are selected and input arrival times of a cell are ignored.

Seit langem ist die Intelligenz des Menschen für viele Forscher und Philosophen ein faszinierendes Forschungsobjekt. Mit dem Aufkommen der Computertechnik erscheint nun zum ersten mal der Traum, einige dieser typisch menschlichen Fähigkeiten nicht nur zu verstehen, sondern nachbauen oder in Teilgebieten gar übertreffen zu können, als realistisch. Ein wichtiger Teil dieses mit "Künstliche Intelligenz" überschriebenen Forschungsgebietes ist das Schließen über Aktionen und Veränderung. Hier wird versucht, die menschliche Fähigkeit, die Effekte seiner Aktionen vorauszusehen und Pläne zum Erreichen von Zielen zu schmieden, nachzubilden. Ein aktives Forschungsgebiet in diesem Rahmen ist der Fluentkalkül, ein Formalismus zur Modellierung von Aktionen und Veränderung. Er stellt Mittel bereit, in der ein automatischer Agent seine Umgebung und die Effekte seiner Aktionen im Rahmen der mathematischen Logik darstellen kann, um mit Hilfe von logischem Schließen sein Verhalten zu planen. Obwohl zum Fluentkalkül viele Arbeiten existieren, die dessen Anwendungsbereiche und Semantik erweitern, gibt es doch noch relativ wenige Arbeiten zum effizienten Schlussfolgern. Dies ist ein Hauptaugenmerk der vorliegenden Arbeit. Es wird ein Algorithmus geschaffen, der Erkenntnisse aus effizienten Verfahren zum Modelchecking mit Binären Entscheidungsdiagrammen (BDDs) sinngemäß überträgt und für ein Fragment des Fluentkalkül erweitert. Damit können nun auch Planungsprobleme von Fluentkalkül-Planern gelöst werden, die der realisierten symbolischen Breitensuche besser zugänglich sind, als der bisher aussschliesslich verwendeten heuristischen Tiefensuche. Um eine leichtere Vergleichbarkeit Fluentkalkül-basierter Planungsverfahren mit anderen Planungsalgorithmen zu ermöglichen, wurde eine Übersetzung des ADL-Fragments der Planungsdomänenbeschreibungssprache PDDL in den Fluentkalkül geschaffen. Damit können zahlreiche Planungsprobleme aus der Literatur und Planungsdomänenbibliotheken auch mit Fluentkalkül-Planern bearbeitet werden. Die Übersetzung kann zugleich als formale Semantik des nur informal spezifizierten PDDL dienen.

Cette thèse traite des approches implicites et explicites, ainsi que de leur convergence, de l'exploration d'espace d'états atteignables de circuits logiques provenant de programmes réactifs synchrones écrits en Esterel, ECL ou SyncCharts. Nos travaux visent à réduire les coûts de ces explorations à l'aide de<br />techniques génériques ou spécifiques à notre cadre de travail. Nous utilisons les résultats de ces explorations à des fins de vérification formelle de propriétés de sûreté, de génération d'automates explicites ou de génération de séquences de tests exhaustives. Nous décrivons trois outils.<br />Le premier outil est un vérificateur formel implicite, à base de Diagrammes de Décisions Binaires (BDDs). Ce vérificateur présente plusieurs techniques permettant de réduire le nombre de variables impliquées dans les calculs d'espace d'états. Nous proposons notamment l'abstraction de variables à l'aide d'une logique trivaluée. Cette nouvelle méthode étend la technique usuelle de remplacement de variables d'états par des entrées libres. Ces deux méthodes calculant des sur-approximations de l'espace d'états atteignables, nous proposons différentes techniques utilisant des informations concernant la structure du modèle et permettant de réduire la sur-approximation.<br />Le deuxième outil est un moteur d'exploration explicite, basé sur l'énumération des états accessibles.<br />Ce moteur repose sur la simulation de la propagation du courant électrique dans les portes du circuit et supporte les circuits cycliques. Ce moteur comporte de nombreuses optimisations et fait appel à différentes heuristiques visant à éviter les explosions en temps ou en espace inhérentes à cette approche, ce qui lui<br />confère de très bonnes performances. Ce moteur a été appliqué à la génération d'automates explicites et à la vérification formelle.<br />Enfin, le troisième outil est une évolution hybride implicite/explicite du moteur purement explicite. Dans cette évolution, les états sont toujours analysés individuellement mais symboliquement à l'aide de BDDs. Ce moteur a également été appliqué à la génération d'automates explicites, mais il est plutôt destiné à la vérification formelle ou la génération de séequences de tests exhaustives.<br />Nous présentons des résultats d'expérimentations de ces différentes approches sur plusieurs exemples industriels.