Browsing by Subject "formal verification"
Now showing 1 - 3 of 3
Results Per Page
Sort Options
Item Design, Implementation, and Formal Verification of On-demand Connection Establishment Scheme for TCP Module of MPICH2 Library(2012-10-19) Muthukrishnan, Sankara SubbiahMessage Passing Interface (MPI) is a standard library interface for writing parallel programs. The MPI specification is broadly used for solving engineering and scientific problems on parallel computers, and MPICH2 is a popular MPI implementation developed at Argonne National Laboratory. The scalability of MPI implementations is very important for building high performance parallel computing applications. The initial TCP (Transmission Control Protocol) network module developed for Nemesis communication sub-system in the MPICH2 library, however, was not scalable in how it established connections: pairwise connections between all of an application's processes were established during the initialization of the application (the library call to MPI_Init), regardless of whether the connections were eventually needed or not. In this work, we have developed a new TCP network module for Nemesis that establishes connections on-demand. The on-demand connection establishment scheme is designed to improve the scalability of the TCP network module in MPICH2 library, aiming to reduce the initialization time and the use of operating system resources of MPI applications. Our performance benchmark results show that MPI_Init in the on-demand connection establishment scheme becomes a fast constant time operation, and the additional cost of establishing connections later is negligible. The on-demand connection establishment between two processes, especially when two processes attempt to connect to each other simultaneously, is a complex task due to race-conditions and thus prone to hard-to-reproduce defects. To assure ourselves of the correctness of the TCP network module, we modeled its design using the SPIN model checker, and verified safety and liveness properties stated as Linear Temporal Logic claims.Item Formal Verification and In-Situ Test of Analog and Mixed-Signal Circuits(2012-08-15) Yin, Leyi 1983-As CMOS technologies continuously scale down, designing robust analog and mixed-signal (AMS) circuits becomes increasingly difficult. Consequently, there are pressing needs for AMS design checking techniques, more specifically design verification and design for testability (DfT). The purpose of verification is to ensure that the performance of an AMS design meets its specification under process, voltage and temperature (PVT) variations and different working conditions, while DfT techniques aim at embedding testability into the design, by adding auxiliary circuitries for testing purpose. This dissertation focuses on improving the robustness of AMS designs in highly scaled technologies, by developing novel formal verification and in-situ test techniques. Compared with conventional AMS verification that relies more on heuristically chosen simulations, formal verification provides a mathematically rigorous way of checking the target design property. A formal verification framework is proposed that incorporates nonlinear SMT solving techniques and simulation exploration to efficiently verify the dynamic properties of AMS designs. A powerful Bayesian inference based technique is applied to dynamically tradeoff between the costs of simulation and nonlinear SMT. The feasibility and efficacy of the proposed methodology are demonstrated on the verification of lock time specification of a charge-pump PLL. The powerful and low-cost digital processing capabilities of today?s CMOS technologies are enabling many new in-situ test schemes in a mixed-signal environment. First, a novel two-level structure of GRO-PVDL is proposed for on-chip jitter testing of high-speed high-resolution applications with a gated ring oscillator (GRO) at the first level to provide a coarse measurement and a Vernier-style structure at the second level to further measure the residue from the first level with a fine resolution. With the feature of quantization noise shaping, an effective resolution of 0.8ps can be achieved using a 90nm CMOS technology. Second, the reconfigurability of recent all-digital PLL designs is exploited to provide in-situ output jitter test and diagnosis abilities under multiple parametric variations of key analog building blocks. As an extension, an in-situ test scheme is proposed to provide online testing for all-digital PLL based polar transmitters.Item A self-verifying theorem prover(2009-12) Davis, Jared Curran; Moore, J Strother, 1947-; Emerson, E. Allen; Harrison, John; Hunt, Jr., Warren A.; Kaufmann, Matt; Lifschitz, VladimirPrograms have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true"). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof---that is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs. In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1.