Innovative nano-scale devices have been developed to enhance future circuit design to overcome physical barriers hindering complementary metal-oxide semiconductor (CMOS) technology. Among the emerging nanodevices, resonant tunneling diodes (RTDs) have demonstrated promising electronic features due to their high speed switching capability and functional versatility. Great circuit functionality can be achieved through integrating heterostructure field-effect transistors (HFETs) in conjunction with RTDs to modulate effective negative differential resistance (NDR). However, RTDs are intrinsically suitable for implementing threshold logic rather than Boolean logic which has dominated CMOS technology in the past. To fully take advantage of such emerging nanotechnology, efficient design methodologies and design automation tools for threshold logic therefore become essential. In this thesis, we first propose novel programmable logic elements (PLEs) implemented in threshold gates (TGs) and multi-threshold threshold gates (MTTGs) by exploring RTD/ HFET monostable-bistable transition logic element (MOBILE) principles. Our three-input PLE can be configured through five control bits to realize all the three-variable logic functions, which is, to the best of our knowledge, the first single RTD-based structure that provides complete logic implementation. It is also a more efficient reconfigurable circuit element than a general look-up table which requires eight configuration bits for three-variable functions. We further extend the design concept to construct a more versatile four-input PLE. A comprehensive comparison of three- and four-input PLEs provides an insightful view of design tradeoffs between performance and area. We present the mathematical proof of PLE's logic completeness based on Shannon Expansion, as well as the HSPICE simulation results of the programmable and primitive RTD/HFET gates that we have designed. An efficient control bit generating algorithm is developed by using a special encoding scheme to implement any given logic function. In addition, we propose novel techniques of formulating a given threshold logic in conjunctive normal form (CNF) that facilitates efficient SAT-based equivalence checking for threshold logic networks. Three different strategies of CNF generation from threshold logic representations are implemented. Experimental results based on MCNC benchmarks are presented as a complete comparison. Our hybrid algorithm, which takes into account input symmetry as well as input weight order of threshold gates, can efficiently generate CNF formulas in terms of both SAT solving time and CNF generating time. / Master of Science

Programmed Cell Death, or Apoptosis, plays a critical role in human embryonic development and in adult tissue homeostasis. Recent research efforts in Bioinformatics and Computational Biology focus on gaining deep insight into the Apoptosis process. This allows researchers to clearly study the relation between the dysregulation of apoptosis and the development of cancer. Research in this highly interdisciplinary field of bioinformatics has become much more quantitative, using tools from computational sciences to understand the behavior of Biological systems. Previously, an abstracted model has been developed to study the Apoptosis process as a Finite State Discrete Transition Model. This model facilitates the reutilization of the digital design verification and testing techniques developed in the Electronic Design Automation domain. These verification and testing techniques for hardware have become robust over the past few decades. Usually simulation is the cornerstone of the Design Verification industry and bulk of states are covered by simulation. Formal verification techniques are then used to analyze the remaining corner case states. Techniques like Genetic Algorithm guided Logic Simulation (GALS) and SAT-based Induction have already been applied to the Apoptosis Discrete Transition Model. However, the Apoptosis model presents some unique problems. The simulation techniques have shown to be unable to cover most of the states of the Apoptosis model. When SAT-based Induction is applied to the Apoptosis model, in particular to find illegal states, very few illegal states are identified. It particularly suffers from the fact that the Apoptosis Model is rather complex and the formulation for testing and verification is hard to tackle at larger bounds greater than 20 or so. Consequently, the state space of the Apoptosis model largely lies in the unknown region, meaning that we are unable to either reach those states or prove that they are illegal. Unless we know whether these states are reachable or illegal, it is not feasible to infer information about the model such as what protein concentrations can be reached under what kind of input stimuli. Questions such as whether certain protein concentrations can be reached or not in this model can only be answered if we have a clear picture of the reachability of state space. In this thesis, we propose techniques based on ATPG and SAT based image computation of the Apoptosis finite transition model. Our method leverages the results obtained in previous research work. It uses the reachable states obtained from the simulation traces of the previous work as initial states for our technique. This enables us to identify more illegal states in less number of iterations; in other words, we are able to reach the fixed point in image computation faster. Our experimental analysis illustrates that the proposed techniques could prove most of the former unknown states as illegal states. We are able to extend our analysis to obtain clearer picture of the interaction of any two proteins in the system considered together. / Master of Science

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.

Programmers often have to spend a significant amount of time inspecting the software code and execution traces to identify the root cause of a software bug. For a multithreaded program, debugging is even more challenging due to the subtle interactions between concurrent threads and the often astronomical number of possible interleavings. In this work, we propose a logical constraint-based symbolic analysis method to aid in the diagnosis of concurrency bugs and find their root causes, which can be later used to recommend repairs. In our method, the diagnosis process is formulated as a set of constraint solving problems. By leveraging the power of constraint satisfiability (SAT) solvers and a bounded model checker, we perform a semantic analysis of the sequential computation as well as the thread interactions. The analysis is ideally suited for handling software with small to medium code size but complex concurrency control, such as device drivers, synchronization protocols, and concurrent data structures. We have implemented our method in a software tool and demonstrated its effectiveness in diagnosing subtle concurrency bugs in multithreaded C programs. / Master of Science

Automatically calculating periodic timetables in public railway transport systems is an NP-complete problem – namely the Periodic Event Scheduling Problem (PESP). The original model is restricted to basic periodic timetabling. Extending the model by decisional transport networks with flows induces new possibilities in the timetabling and planning process. Subsequently, the given flexibility results in a generic model extension of PESP that can be applied in subsets of the timetabling process. The successful utilization of this approach is presented for distinct chain paths, duplicated chain paths and non-connected flow graphs that represent integration of routing and timetabling, planning of periodic rail freight train paths and track allocation, respectively. Furthermore, the encoding of this generic model into a binary propositional formula is introduced and the appropriate usage of several techniques like SAT solving and MaxSAT to calculate and optimize the corresponding instances will be presented accordingly. Computational results for real-world scenarios suggest the practical impact and give promising perspectives for further scientific research.

Many formal descriptions of DPLL-based SAT algorithms either do not include all essential proof techniques applied by modern SAT solvers or are bound to particular heuristics or data structures. This makes it difficult to analyze proof-theoretic properties or the search complexity of these algorithms. In this paper we try to improve this situation by developing a nondeterministic proof calculus that models the functioning of SAT algorithms based on the DPLL calculus with clause learning. This calculus is independent of implementation details yet precise enough to enable a formal analysis of realistic DPLL-based SAT algorithms. / Viele formale Beschreibungen DPLL-basierter SAT-Algorithmen enthalten entweder nicht alle wesentlichen Beweistechniken, die in modernen SAT-Solvern implementiert sind, oder sind an bestimmte Heuristiken oder Datenstrukturen gebunden. Dies erschwert die Analyse beweistheoretischer Eigenschaften oder der Suchkomplexität derartiger Algorithmen. Mit diesem Artikel versuchen wir, diese Situation durch die Entwicklung eines nichtdeterministischen Beweiskalküls zu verbessern, der die Arbeitsweise von auf dem DPLL-Kalkül basierenden SAT-Algorithmen mit Klausellernen modelliert. Dieser Kalkül ist unabhängig von Implementierungsdetails, aber dennoch präzise genug, um eine formale Analyse realistischer DPLL-basierter SAT-Algorithmen zu ermöglichen.

Die Expression von natriumabhängigen und natriumunabhängigen Transportern für Sulfat in Nieren und Leber ist für die Sulfathomöostase unabdingbar. Ein natriumunabhängiger Transporter für Sulfat ist der Sulfat-Anionen-Transporter 1, sat-1, der Sulfat im Austausch gegen Oxalat, Bicarbonat, Chlorid und Glyoxylat sowohl in die Zellen aufnehmen als auch in das Blut abgeben kann. In dieser Arbeit wurde die Transportfunktion des Sulfat-Anionen-Transporters 1 der Ratte, rsat-1, untersucht. Das Ziel war eine genauere Kenntnis über den Einfluss von Chlorid, des intrazellulären pH-Wertes und der extrazellulären Calciumkonzentration auf den Sulfattransport durch rsat-1 zu erlangen. Als Expressionssystem für rsat-1 wurden Oozyten des Krallenfrosches Xenopus-laevis verwendet. Elektrophysiologische Versuche, die im „Current-Clamp-Modus“ durchgeführt wurden, ermöglichten die Messung von substratinduzierten Potentialänderungen. Durch radiochemische Versuche konnte die Sulfataufnahme durch sat-1 unter variierenden Bedingungen bestimmt werden. Die Rolle des Chlorids in Hinblick auf den Sulfattransport durch sat-1 konnte nicht gänzlich geklärt werden. Da Thiosulfat und Nitrat in den durchgeführten Versuchen die Aufnahme von [35S]Sulfat über rsat-1 hemmten, könnte das Stickstoffatom den Transport von Sulfat beeinflussen. Intrazellulär an Chlorid verarmte rsat-1-exprimierende Oozyten nahmen in den durchgeführten Versuchen vermehrt [35S]Sulfat auf. Des Weiteren konnte eine Steigerung der [35S]Sulfataufnahme in chloridreduzierten, gluconat- beziehungsweise mannithaltigen Lösungen beobachtet werden. Die Ergebnisse dieser Arbeit sind mit einer allosterischen oder kompetitiven Hemmung der Aufnahme von Sulfat durch Chlorid vereinbar. Eine genauere Untersuchung des Chloridtransports über sat-1 wäre durch Versuche mit radioaktiv markiertem Iod¹²⁵ möglich, das wie Chlorid transportiert wird. Die intrazelluläre Ansäuerung der Oozyten durch Ammoniumchlorid führte zu einer erhöhten [35S]Sulfataufnahme in die rsat-1-exprimierenden Oozyten. Diese könnte durch eine verminderte Bicarbonatkonzentration an der äußeren Zellmembran mit einer reduzierten kompetitiven Hemmung begründet sein. Ebenso könnte Ammoniumchlorid durch eine protonierende Wirkung eine Konformationsänderung mit einer Affinitätssteigerung von sat-1 für Sulfat zur Folge haben. Mit steigender Calciumkonzentration wurde die Depolarisation rsat-1-exprimierender Oozyten in chloridreduzierten und gluconathaltigen Lösungen geringer. Dies ist mit bereits vorliegenden Daten vereinbar, in denen Xenopus laevis Oozyten in chloridreduzierten Medien depolarisieren.

Boolean satisfiability (SAT) is the problem of determining whether there exists an assignment of the Boolean variables to the truth values such that a given Boolean formula evaluates to true. SAT was the first example of an NP-complete problem. Only two decades ago SAT was mainly considered as of a theoretical interest. Nowadays, the picture is very different. SAT solving becomes mature and is a successful approach for tackling a large number of applications, ranging from artificial intelligence to industrial hardware design and verification. SAT solving consists of encodings and solvers. In order to benefit from the tremendous advances in the development of solvers, one must first encode the original problems into SAT instances. These encodings should not only be easily generated, but should also be efficiently processed by SAT solvers. Furthermore, an increasing number of practical applications in computer science can be expressed as constraint satisfaction problems (CSPs). However, encoding a CSP to SAT is currently regarded as more of an art than a science, and choosing an appropriate encoding is considered as important as choosing an algorithm. Moreover, it is much easier and more efficient to benefit from highly optimized state-of-the-art SAT solvers than to develop specialized tools from scratch. Hence, finding appropriate SAT encodings of CSPs is one of the most fascinating challenges for solving problems by SAT. This thesis studies SAT encodings of CSPs and aims at: 1) conducting a comprehensively profound study of SAT encodings of CSPs by separately investigating encodings of CSP domains and constraints; 2) proposing new SAT encodings of CSP domains; 3) proposing new SAT encoding of the at-most-one constraint, which is essential for encoding CSP variables; 4) introducing the redundant encoding and the hybrid encoding that aim to benefit from both two efficient and common SAT encodings (i.e., the sparse and order encodings) by using the channeling constraint (a term used in Constraint Programming) for SAT; and 5) revealing interesting guidelines on how to choose an appropriate SAT encoding in the way that one can exploit the availability of many efficient SAT solvers to solve CSPs efficiently and effectively. Experiments show that the proposed encodings and guidelines improve the state-of-the-art SAT encodings of CSPs.

A constraint is a formula in first-order logic expressing a relation between values of various domains. In order to solve a constraint, constructing a propositional encoding is a successfully applied technique that benefits from substantial progress made in the development of modern SAT solvers. However, propositional encodings are generally created by developing a problem-specific generator program or by crafting them manually, which often is a time-consuming and error-prone process especially for constraints over complex domains. Therefore, the present thesis introduces the constraint solver CO4 that automatically generates propositional encodings for constraints over structured finite domains written in a syntactical subset of the functional programming language Haskell. This subset of Haskell enables the specification of expressive and concise constraints by supporting user-defined algebraic data types, pattern matching, and polymorphic types, as well as higher-order and recursive functions. The constraint solver CO4 transforms a constraint written in this high-level language into a propositional formula. After an external SAT solver determined a satisfying assignment for the variables in the generated formula, a solution in the domain of discourse is derived. This approach is even applicable for finite restrictions of recursively defined algebraic data types. The present thesis describes all aspects of CO4 in detail: the language used for specifying constraints, the solving process and its correctness, as well as exemplary applications of CO4.

No description available.