Browsing by Subject "Integrated circuits--Verification"

Now showing 1 - 5 of 5

Automatic structural abstraction techniques for enhanced verification
(2002-12) Baumgartner, Jason Raymond; Abraham, Jacob A.
Computers have become central components of nearly every facet of modern life. Advances in hardware development have resulted in computers more powerful than the largest mainframe of the last decade becoming available and affordable for general use. This in turn has enabled problems which were historically intractable to become solvable with present technologies. This trend has been noted for four decades. Functional verification is the process of validating that a design conforms to its specification. Exhaustive verification generally requires exponential resources with respect to design size, hence there is a fine line between “solvable” and “intractable”; this cut-off point is unfortunately often far smaller than that which is practically necessary. Due to ongoing increases in hardware design size, direct application of exhaustive techniques to verify these designs requires exponentially-growing verification resources which outpaces available boosts in computing power. Therefore, on the surface, Moore’s law works against the hardware verification community. This thesis presents an approach to battling verification complexity via automatic abstraction techniques which transform the structure of a design. These techniques require ix only polynomial resources with respect to design size, and may yield exponential speedups to the verification process. These abstractions are developed as components of a modular transformation-based verification framework, enabling optimal synergy between the various techniques. Our specific contributions include: 1) a compositional and structural diameter overapproximation technique, enabling the use of abstractions to tighten the produced bounds; 2) an on-the-fly retiming technique for redundancy removal; 3) the concept of fanin register sharing to enhance min-area retiming; 4) a generalized retiming approach which eliminates reset state and input-output equivalence constraints, and supports negative registers; 5) structural cut-based abstraction; 6) a structural target enlargement approach; 7) the technique of -slow abstraction; and 8) the technique of phase abstraction. Numerous experiments demonstrate the utility and synergy of these techniques in simplifying difficult problems. We therefore feel that these techniques comprise a significant step towards a scalable, automated verification system, helping to realize the prediction made by E. Allen Emerson that “Someday, Moore’s Law will work for us [the verification community], rather than against us.”
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.
Improving timing verification and delay testing methodologies for IC designs
(2005) Zeng, Jing; Abraham, Jacob A.
The task of ensuring the correct temporal behavior of IC designs, both before and after fabrication, is extremely important. It is becoming even more imperative as the demand for performance increases and process technology advances into the deep sub-micron region. This dissertation tackles the key issues in the timing verification and delay testing methodologies. An efficient methodology is presented to identify false timing paths in the timing verification methodology which utilizes ATPG technique and timing information from an ordered list of timing paths according to the delay information. This dissertation also presents a speed binning methodology which utilizes structural delay tests successfully instead of functional tests. In addition, it establishes a methodology which quantifies the correlation between the timing verification prediction and actual silicon measurement of timing paths. This quantification methodology lays the foundation for further research to study the impact of deep submicron effects on design performance
Symbolic methods in simulation-based verification
(2002) Yuan, Jun; Aziz, Adnan
This dissertation conducts research in automating the design of digital hard- ware. Specifically we apply symbolic methods in simulation-based functional ver- ification. Simulation, due to its simplicity and close coupling with the electronic design process, has been the prevalent approach to checking the correctness of de- signs. However, it suffers from several drawbacks. First, simulation verifies only the portion of design behavior that is exercised by input vectors; in addition, input vector generation itself is a time-consuming and error-prone process. Both prob- lems are aggravated by the exponential growth in integrated circuit design com- plexity. On the other side, formal verification is “vector-less” in that it certifies cor- rectness either through mathematically rigorous proofs, or by exhaustive enumera- tion of design behaviors. Needless to mention, this approach requires either enor- mous computation resources or a great deal of manual intervention to verify large designs. The problem, however, is greatly alleviated by the advent of symbolic methods, particularly the introduction of Binary Decision Diagrams to represent sets of state and transition dynamics. Symbolic formal verification has since been adopted in practice, but still limited to simple protocols and small designs. It is natural to explore ways to leverage symbolic methods in simulation verification. To this end, we introduce several such applications. We first describe what we referred to as “saturated simulation” and “retrograde analysis” in checking invariant properties that are common to electronics designs. State and transition coverage are used as the guidance for a partial symbolic simulation. Consequently, a higher level of verification confidence is achieved. We then present a symbolic input vector generation method, in which state- dependent constraints and input biases are used to confine the generated vectors to “legal” and “interesting” cases. The constraints and biases are both of a dynamic nature, that is, they can depend upon the state of the design. This enables generation of complicated sequences of vectors. We also discuss methods of optimizing the vector generation process through efficient extraction of a special kind of constraints, in which the inputs are fully specified by the state of the design. In the end, we present an alternative vector gen- eration method based on constraint synthesis. Beyond its obvious role in simulation, the method also provides a constraint based interface model for other verification approaches, such as model checking and emulation.
Using theorem proving and algorithmic decision procedures for large-scale system verification
(2005) Ray, Sandip; Moore, J Strother, 1947-
The goal of formal verification is to use mathematical methods to prove that a computing system meets its specifications. When applicable, it provides a higher assurance than simulation and testing in correct system execution. However, the capacity of the state of the art in formal verification today is still far behind what is necessary for its widespread adoption in practice. In this dissertation, we devise methods to increase the capacity of formal verification. Formal verification techniques can be broadly divided into two categories, namely deductive techniques or theorem proving, and decision procedures such as model checking, equivalence checking, and symbolic trajectory evaluation. Neither deductive nor algorithmic techniques individually scale up to the size of modern industrial systems, albeit for orthogonal reasons. Decision procedures suffer from state explosion. Theorem proving requires manual assistance. Our methods involve a sound, efficient, and scalable integration of deductive and algorithmic techniques. ix There are four main contributions in this dissertation. First, we present several results that connect different deductive proof styles used in the verification of sequential programs. The connection allows us to efficiently combine theorem proving with symbolic simulation to prove the correctness of sequential programs without requiring a verification condition generator or manual construction of a global invariant. Second, we formalize a notion of correctness for reactive concurrent programs that affords effective reasoning about infinite computations. We discuss several reduction techniques that reduce the correctness proofs of concurrent programs to the proof of an invariant. Third, we present a method to substantially automate the process of discovering and proving invariants of reactive systems. The method combines term rewriting with reachability analysis to generate efficient predicate abstractions. Fourth, we present an approach to integrate model checking procedures with deductive reasoning in a sound and efficient manner. We use the ACL2 theorem prover to demonstrate our methods. A consequence of our work is the identification of certain limitations in the logic and implementation of ACL2. We recommend several augmentations of ACL2 to facilitate deductive verification of large systems and integration with decision procedures.