Zugl.: Darmstadt, Techn. Univ., Diss., 2006

Techn. Univ., Diss--Darmstadt, 2006.

University, Diss., 2002--Kiel.

Techn. University, Diss., 2003--Kaiserslautern.

Zugl.: Bremen, Univ., Diss., 2009

Zugl.: Bremen, Univ., Diss., 2007

With the ever increasing complexity of digital systems, functional verification has become a daunting task to circuit designers. Functional verification alone often surpasses 70% of the total development cost and the situation has been projected to continue to worsen. The most critical limitations of existing techniques are the capacity issue and the run-time issue. This dissertation addresses the functional verification problem using a unified approach, which utilizes different core algorithms at various abstraction levels. At the logic level, we focus on incorporating a set of novel ideas to existing formal verification approaches. First, we present a number of powerful optimizations to improve the performance and capacity of a typical SAT-based bounded model checking framework. Secondly, we present a novel method for performing dynamic abstraction within a framework for abstraction-refinement based model checking. Experiments on a wide range of industrial designs have shown that the proposed optimizations consistently provide between 1-2 orders of magnitude speedup and can be extremely useful in enhancing the efficacy of existing formal verification algorithms. At the register transfer level, where the formal verification is less likely to succeed, we developed an efficient ATPG-based validation framework, which leverages the high-level circuit information and an improved observability-enhanced coverage to generate high quality validation sequences. Experiments show that our approach is able to generate high quality validation vectors, which achieve both high tag coverage and high bug coverage with extremely low computational cost. / Ph. D.

Conventional testing has become inadequate to satisfy rigorous reliability requirements of embedded software that is playing an increasingly important role in many safety critical applications. Automatic formal verification is a viable avenue for ensuring the reliability of such software. Recently, more and more formal verification techniques have begun modeling a non-Boolean data variable as a bit-vector with bounded width (i.e. a vector of multiple bits like 32- or 64- bits) to implement bit-precise verification. One major challenge in the scalable application of such bit-precise verification on real-world embedded software is that the state space for verification can be intractably large. In this dissertation, several abstraction techniques are explored to deal with this scalability challenge in the bit-precise verification of embedded software. First, we propose a tight integration of program slicing, which is an important static program analysis technique, with bounded model checking (BMC). While many software verification tools apply program slicing as a separate preprocessing step, we integrate slicing operations into our model construction and reduction process and enhance them with compilation optimization techniques to compute accurate program slices. We also apply a proof-based abstraction-refinement framework to further remove those program segments irrelevant to the property being verified. Next, we present a method of using symbolic simulation for scalable formal verification. The simulation involves distinguishing X as symbolic values to abstract concrete variables' values. Also, the method embeds this symbolic simulation in a counterexample-guided abstraction-refinement framework to automatically construct and verify an abstract model, which has a smaller state space than that of the original concrete program. This dissertation also presents our efforts on using two common testability metrics — controllability metric (CM) and observability metric (OM) — as the high-level structural guidance for scalable bit-precise verification. A new abstraction approach is proposed based on the concept of under- and over-approximation to efficiently solve bit-vector formulas generated from embedded software verification instances. These instances include both complicated arithmetic computations and intensive control structures. Our approach applies CM and OM to assist the abstraction refinement procedure in two ways: (1) it uses CM and OM to guide the construction of a simple under-approximate model, which includes only a subset of execution paths in a verification instance, so that a counterexample that refutes the instance can be obtained with reduced effort, and (2) in order to reduce the cost of using proof-based refinement alone, it uses OM heuristics to guide the restoration of additional verification-relevant formula constraints with low computational cost for refinement. Experiments show a significant reduction of the solving time compared to state-of-the-art solvers for the bit-vector arithmetic. This dissertation finally proposes an efficient algorithm to discover non-uniform encoding widths of individual variables in the verification model, which may be smaller than their original modeling width but sufficient for the verification. Our algorithm distinguishes itself from existing approaches in that it is path-oriented; it takes advantage of CM and OM values to guide the computation of the initial, non-uniform encoding widths, and the effective adjustment of these widths along different paths, until the property is verified. It can restrict the search from those paths that are deemed less favorable or have been searched in previous steps, thus simplifying the problem. Experiments demonstrate that our algorithm can significantly speed up the verification especially in searching for a counterexample that violates the property under verification. / 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

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