Browsing by Subject "Formal methods (Computer science)"
Now showing 1 - 5 of 5
Results Per Page
Sort Options
Item Combining advanced formal hardware verification techniques(2007-12) Reeber, Erik Henry, 1978-; Hunt, Warren A., 1958-This dissertation combines formal verification techniques in an attempt to reduce the human effort required to verify large systems formally. One method to reduce the human effort required by formal verification is to modify general-purpose theorem proving techniques to increase the number of lemma instances considered automatically. Such a modification to the forward chaining proof technique within the ACL2 theorem prover is described. This dissertation identifies a decidable subclass of the ACL2 logic, the Subclass of Unrollable List Formulas in ACL2 (SUFLA). SUFLA is shown to be decidable, i.e., there exists an algorithm that decides whether any SUFLA formula is valid. Theorems from first-order logic can be proven through a methodology that combines interactive theorem proving with a fully-automated solver for SUFLA formulas. This methodology has been applied to the verification of components of the TRIPS processor, a prototype processor designed and fabricated by the University of Texas and IBM. Also, a fully-automated procedure for the Satisfiability Modulo Theory (SMT) of bit vectors is implemented by combining a solver for SUFLA formulas with the ACL2 theorem prover's general-purpose rewriting proof technique. A new methodology for combining theorem proving and model checking is presented, which uses a unique "black-box" formalization of hardware designs. This methodology has been used to combine the ACL2 theorem prover with IBM's SixthSense model checker and applied to the verification of a high-performance industrial multiplier design. A general-purpose mechanism has been created for adding external tools to a general-purpose theorem prover. This mechanism, implemented in the ACL2 theorem prover, is capable of supporting the combination of ACL2 with both SixthSense and the SAT-based SUFLA solver. A new hardware description language, DE2, is described. DE2 has a number of unique features geared towards simplifying formal verification, including a relatively simple formal semantics, support for the description of circuit generators, and support for embedding non-functional constructs within a hardware design. The composition of these techniques extend our knowledge of the languages and logics needed for formal verification and should reduce the human effort required to verify large hardware circuit models.Item Efficient and effective symbolic model checking(2006) Iyer, Subramanian Krishnan; Emerson, E. AllenThe main bottleneck in practical symbolic model checking is that it is restricted by the ability to efficiently represent and perform operations on sets of states. Symbolic representations, like Binary Decision Diagrams, grow very large quickly due to their necessity to cover the state space in a breadth first fashion. Satisfiability based techniques result in a proliferation of clauses, one reason being that they have to replicate the transition relation numerous times. We propose techniques to increase the capacity of automatic state-based verification as applied to sequential designs, i.e., symbolic model checking. Firstly, we propose the use of dynamically partitioned ordered Binary Decision Diagrams as a capable data structure. This leads to vast improvements in state space traversal in general and error detection in buggy designs, in particular. Secondly, we propose a partitioned approach to model checking, which splits the problem into multiple partitions handled independently of each other. State space partitioning-based approaches have been proposed in the literature to address the state explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of inter-partition (cross-over) image computations, which can be expensive. We present a model checking algorithm that aggregates these expensive cross-over images by localizing computation to individual partitions. This algorithm is more suited to parallelization than existing model checking approaches. It reduces the number of cross-over images and drastically outperforms extant approaches in terms of cross-over image computation cost as well as total model checking time, often by two orders of magnitude. We address the issue of time scalability in verification, whereby the availability of larger amounts of computation time enables greater exploration of the state space. From a practical standpoint, we observe that extant verification approaches are unable to proceed very deep into the state space. It is our conjecture that partitioning can help in this context and we explore this issue further. Finally, we study the combination of partitioned binary decision diagrams with bounded model checking for more scalable and efficient model checking. We give a technique to scale formal verification to a large grid of processors that demonstrates marked superiority over existing approaches. The contributions of this dissertation are in improving the capacity of symbolic model checking approaches to formal verification, in terms of time and memory requirements, as well as in the development of techniques that are more readily amenable to parallel and distributed model checking.Item Exploiting replication in automated program verification(2007) Wahl, Thomas, 1973-; Emerson, E. AllenThis dissertation shows how systems of many concurrent components, which naively engender intractably large state spaces, can nevertheless be successfully subject to exhaustive formal verification, provided the components can be classified into a few types. It therefore addresses an instance of the state explosion problem: a finite-state model of a system can be much larger than a high-level description of this system. Model checking, the technique to which this dissertation is primarily devoted, inherently relies on state space exploration and thus suffers from this problem more than other formal verification methods. The state explosion phenomenon persists even if the system consists of components that are simply replicated instances of a generic behavioral description. Examples of such systems abound; they include processes executing concurrently according to some common protocol, clusters of processors executing a parallel provii gram, and hardware with replicated physical devices in a uniform arrangement. Fortunately, models of such systems often exhibit a regular structure, known as symmetry, which can be exploited in verification, sometimes to the extent of an exponential reduction in model size. The first contribution of this dissertation is to show how reductions based on symmetry can be performed with state-of-the-art system representations. Many of today’s computing systems induce astronomically large state spaces whose formal models require a symbolic encoding using boolean formulas. Such succinct representations call for new algorithms that can process entire sets of objects at once. How to detect symmetry quickly during symbolic model checking, so that redundancy in the exploration can be avoided, was an open problem for some time. In this dissertation we provide an efficient and flexible solution to this problem by using symbolic data structures in a somewhat unconventional way. The second contribution is to extend symmetry reduction techniques to more realistic and general scenarios. We establish that the principal ideas still apply if symmetry is violated in parts of the state space. Such scenarios are common in practice, for instance when priorities determine which of several competing processes can access a resource first. In these situations it is beneficial to exploit symmetry where it exists and watch out for the (few) violations, rather than to ignore it altogether. We also demonstrate how symmetry can help us solve a practically significant instance of parameterized verification of system families. This technique traditionally attempts to prove properties about systems independently of the size parameter, but requires models of a special structure. We show that by restricting the parameter to a finite range we can solve this problem efficiently, can do so without any conditions on the models’ structure, and can take advantage of symmetry in the individual systems of the family if it exists.Item Generalization, lemma generation, and induction in ACL2(2008-05) Erickson, John D., Ph. D.; Moore, J. Strother, 1947-Formal verification is becoming a critical tool for designing software and hardware today. Rising complexity, along with software's pervasiveness in the global economy have meant that errors are becoming more difficult to find and more costly to fix. Among the formal verification tools available today, theorem provers offer the ability to do the most complete verification of the most complex systems. However, theorem proving requires expert guidance and typically is too costly to be economical for all but the most mission critical systems. Three major challenges to using a theorem prover are: finding generalizations, choosing the right induction scheme, and generating lemmas. In this dissertation we study all three of these in the context of the ACL2 theorem prover.Item High level static analysis of system descriptions for taming verification complexity(2007-12) Vasudevan, Shobha; Abraham, Jacob A.The growing complexity of VLSI and System-on-a-chip(SoC) designs has made their verification extremely expensive, time-consuming and resource intensive. Formal verification of system behavior is critical to the design cycle due to its ability to isolate subtle flaws and provide high quality assurance. However, its computational intractability limits applicability in practice, rendering the state-of-the-art insufficient to meet the needs of the industry. In this dissertation, a suite of techniques that are a significant departure from traditional Boolean level approaches to formal verification are presented. The algorithms are based on a top-down, domain-aware perspective of the system by reasoning at the system level and register transfer level (RTL) descriptions. Static analysis of these high level system descriptions using structural information and symbolic reasoning leads to effective decomposition strategies that create tractable portions of the system. These manageable system components can then be verified by deploying efficient Boolean level algorithms. The techniques presented here apply to the actual RTL source code, and are intended to blend seamlessly into the system design cycle. All approaches using high level static analyis follow a three pronged solution- domain aware analysis, high level symbolic simulation and a decision procedure for the verification task. This work advocates a marked difference in the perspective to formal hardware verification as compared to popular paradigms. The techniques shown here are illustrative of a hardware-aware viewpoint to verification, and argue this case for contemporary verification tasks. Antecedent conditioned slicing, an abstraction technique for reducing RTL design space is introduced. The reduced RTL can then be model checked. An open source RTL implementation of the USB 2.0 protocol is verified using this technique. A technique for pipelined processor verification using antecedent conditioned slicing is introduced. An open source Verilog RTL of OR1200, an embedded processor is explained in a detailed case study for verification using this technique. A static analysis technique is proposed to alleviate the complexity of the sequential equivalence checking problem between system level and RTL descriptions, by efficiently decomposing designs using sequential compare points. A satisfiability (SAT) solver is used as the lower level verification engine. In a case study, sequential equivalence checking between a system level description of a Viterbi decoder and two different RTL implementations are detailed.