An all-digital phase locked loop for WiGig systems was implemented. The developedall-digital phase locked loop has a targeted frequency range of 2.1-GHz to2.5-GHz. The all-digital phase locked loop replaces the traditional charge pumpbased analog phase locked loop. The digital nature of the all-digital phase lockedloop system makes it superior to the analog counterpart.There are four main partswhich constitutes the all-digital phase locked loop. The time-to-digital converteris one of the important block in all-digital phase locked loop. Several time-to-digital converter architectures were studied and simulated. TheVernier delay based architecture and inverter delay based architecture was designedand evaluated. There architectures provided certain short comings whilethe pseudo-differential time-to-digital converter architecture was chosen, becauseof it’s less occupation of area. Since there exists a relationship between the sizeof the delay cells and it’s time resolution, the pseudo-differential time-to-digitalconverter severed it’s purpose. The whole time-to-digital converter system was tested on a 1 V power supply,reference frequency 54-MHz which is also the reference clock Fref , and a feedbackfrequency Fckv 2.1-GHz. The power consumption was found to be around 2.78mW without dynamic clock gating. When the clock gating or bypassing is done,the power consumption is expected to be reduced considerably. The measuredtime-to-digital converter resolution is around 7 ps to 9 ps with a load variation of15 fF. The inherent delay was also found to be 5 ps. The total output noise powerwas found to be -128 dBm.

This thesis is concerned with design and implementation of a complete SAT solver accelerated on GPU. The achitecture of modern graphics cards is described as well as the CUDA platform and a list of common algorithms used for solving the boolean satisfiability problem (the SAT problem). The presented solution is based on the 3-SAT DC alogirthm, which belongs to the family of well-known DPLL based algorithms. This work describes problems encountered during the design and implementation. The resulting application was then analyzed and optimized. The presented solver cannot compete with state of the art solvers, but proves that it can be up to 21x faster than an equivalent sequential version. Unfortunately, the current implementation can only handle formulas of a limited size. Suggestions on further improvements are given in final sections.

No description available.

This paper describes the proof calculus LD for clausal propositional logic, which is a linearized form of the well-known DPLL calculus extended by clause learning. It is motivated by the demand to model how current SAT solvers built on clause learning are working, while abstracting from decision heuristics and implementation details. The calculus is proved sound and terminating. Further, it is shown that both the original DPLL calculus and the conflict-directed backtracking calculus with clause learning, as it is implemented in many current SAT solvers, are complete and proof-confluent instances of the LD calculus. / Dieser Artikel beschreibt den Beweiskalkül LD für aussagenlogische Formeln in Klauselform. Dieser Kalkül ist eine um Klausellernen erweiterte linearisierte Variante des bekannten DPLL-Kalküls. Er soll dazu dienen, das Verhalten von auf Klausellernen basierenden SAT-Beweisern zu modellieren, wobei von Entscheidungsheuristiken und Implementierungsdetails abstrahiert werden soll. Es werden Korrektheit und Terminierung des Kalküls bewiesen. Weiterhin wird gezeigt, dass sowohl der ursprüngliche DPLL-Kalkül als auch der konfliktgesteuerte Rücksetzalgorithmus mit Klausellernen, wie er in vielen aktuellen SAT-Beweisern implementiert ist, vollständige und beweiskonfluente Spezialisierungen des LD-Kalküls sind.

Graduation date: 2006 / Digital phase-locked loops (PLLs) have been receiving increasing attention recently due to their ease of integration, scalability and performance comparable to their analog counterparts. In digital PLLs, increased resolution in time-to-digital conversion is desirable for improved noise performance. This work describes the design and simulation of a stochastic time-to-digital converter (STDC) for a digital PLL to attain high resolution. The converter is intended to comprise the fine loop of the phase-frequency detector, whose coarse loop would be comprised of a time-to-digital converter designed using the conventional delay-chain approach. The STDC is designed, simulated and sent for fabrication in a 0.35μm SOI CMOS process. System level simulations in MATLAB are verified by device level simulations in Spectre on circuits extracted from layout. The results support the viability of using the proposed circuit for high resolution time-to-digital conversion.

xii, 136 p. : ill. A print copy of this thesis is available through the UO Libraries. Search the library catalog for the location and call number. / Many algorithms are known to work well in practice on a variety of different problem instances. Reusing existing algorithms for problems besides the one that they were designed to solve is often quite valuable. This is accomplished by transforming an instance of the new problem into an input for the algorithm and transforming the output of the algorithm into the correct answer for the new problem. To capitalize on the efficiency of the algorithm, it is essential that these transformations are efficient. Clearly not all problems will have efficient transformations to a particular algorithm so there are limitations on the scope of an algorithm. There is no previous study of which I am aware on determining the capability of an algorithm in terms of the complexity of problems that it can be used to solve. Two examples of this concept will be presented in proving the exact capability of the most well known algorithms for solving Satisfiability (SAT) and for solving Quantified Boolean Formula (QBF). The most well known algorithm for solving SAT is called DPLL. It has been well studied and is continuously being optimized in an effort to develop faster SAT solvers. The amount of work being done on optimizing DPLL makes it a good candidate for solving other problems. The notion of algorithm capability proved useful in applying DPLL to two areas of AI: Planning and Nonmonotonic Reasoning. Planning is PSPACE Complete in general, but NP Complete when restricted to problems that have polynomial length plans. Trying to optimize the plan length or introducing preferences increases the complexity of the problem. Despite the fact that these problems are harder than SAT, they are with in the scope of what DPLL can handle. Most problems in nonmonotonic reasoning are also harder than SAT. Despite this fact, DPLL is a candidate solution for nonmonotonic logics. The complexity of nonmonotonic reasoning in general is beyond the scope of what DPLL can handle. By knowing the capability of DPLL, one can analyze subsets of nonmonotonic reasoning that it can be used to solve. For example, DPLL is capable of solving the problem of model checking in normal default logic. Again, this problem is harder than SAT, but can still be solved with a single call to a SAT solver. The idea of algorithm capability led to the fascinating discovery that SAT solvers can solve problems that are harder than SAT. / Advisers: Matthew Ginsberg, Christopher Wilson

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.

O Objetivo deste trabalho foi implementar um resolvedor distribuído para o problema de satisfabilidade em lógica proposicional (SAT) que pudesse ser executado em uma grade de computadores. Foi analisada a influência que o número de máquinas utilizadas pela grade para resolver diversas instâncias do SAT exerce sobre o desempenho do resolvedor implementado / O Objetivo deste trabalho foi implementar um resolvedor distribuído para o problema de satisfabilidade em lógica proposicional (SAT) que pudesse ser executado em uma grade de computadores. Foi analisada a influência que o número de máquinas utilizadas pela grade para resolver diversas instâncias do SAT exerce sobre o desempenho do resolvedor implementado

An increasing number of applications in verification and security rely on or could benefit from automatic solvers that can check the satisfiability of constraints over a rich set of data types that includes character strings. Unfortunately, most string solvers today are standalone tools that can reason only about some fragment of the theory of strings and regular expressions, sometimes with strong restrictions on the expressiveness of their input language (such as, length bounds on all string variables). These specialized solvers reduce string problems to satisfiability problems over specific data types, such as bit vectors, or to automata decision problems. On the other side, despite their power and success as back-end reasoning engines, general-purpose Satisfiability Modulo Theories (SMT) solvers so far have provided minimal or no native support for string reasoning. This thesis presents a deductive calculus describing a new algebraic approach that allows solving constraints over the theory of unbounded strings and regular expressions natively, without reduction to other problems. We provide proofs of refutation soundness and solution soundness of our calculus, and solution completeness under a fair proof strategy. Moreover, we show that our calculus is a decision procedure for the theory of regular language membership with length constraints. We have implemented our calculus as a string solver for the theory of (unbounded) strings with concatenation, length, and membership in regular languages, and incorporated it into the SMT solver CVC4 to expand its already large set of built-in theories. This work makes CVC4 the first SMT solver that is able to accept and process a rich set of mixed constraints over strings, integers, reals, arrays and other data types. In addition, our initial experimental results show that, over string problems, CVC4 is highly competitive with specialized string solvers with a comparable input language. We believe that the approach we described in this thesis provides a new idea for string-based formal methods.

As Moore���s Law continues to give rise to ever shrinking channel lengths, circuits are becoming more digital and ever increasingly faster. Generating high frequency clocks in such scaled processes is becoming a tough challenge. Digital phase locked loops (DPLLs) are being explored as an alternative to conventional analog PLLs but suffer from issues such as low bandwidth and higher quantization noise. A digital multiplying delay locked loop (DMDLL) is proposed which aims at leveraging the benefit of high bandwidth of DLL while at the same time achieving the frequency multiplication property of PLL. It also offers the benefits of easier portability across process and occupies lesser area. The proposed DMDLL uses a simple flip-flop as 1-bit TDC (Time Digital Converter) for Phase Detector (PD). A digital accumulator acts as integrator for loop filter while a ��-�� DAC in combination with a VCO acts like a DCO. A carefully designed select logic in conjunction with a MUX achieves frequency multiplication. The proposed digital MDLL is taped out in 130nm process and tested to obtain 1.4GHz output frequency with 1.6ps RMS jitter, 17ps peak-to-peak jitter and -50dbC/Hz reference spurs. / Graduation date: 2012