The integration of automated techniques for the formal verification of sequential circuits into the design cycle is imperative to handle today's complex circuits. This thesis presents a unified framework for the multilevel verification of sequential circuits viewed as finite state machines. Experimental results are presented on designs from industry.
Verification of circuit implementations against their specifications (circuit descriptions at a higher level in the design hierarchy) is formulated as checking for containment of the specification state machine in the implementation state machine to ensure that all specified behavior is correctly implemented. The concept of strong containment is introduced to exploit correspondences between data registers of descriptions at different stages in the design cycle. It is also shown that containment can be checked by considering subsets of outputs, thus reducing the sizes of the Binary Decision Diagrams used to represent the output functions for large circuits. The concept of strong containment is extended to verify circuits after retiming transformations which destroy the simple data register correspondences.
A framework is also presented for the specification of correctness properties as labeled state machines to aid the designer in verifying the behavioral circuit descriptions which serve as top-level specifications in the design cycle. Algorithms have been developed and implemented for generating counterexamples and witnesses to help in debugging the design. In addition, the applicability of formal techniques to improve simulation-based verification is shown in the form of an Extracted Control Flow Machine model. This model, extracted automatically, embodies the flow of control in a sequential circuit and is used to evaluate the control flow coverage of the simulation vectors used for design verification.
The power of theorem proving techniques in handling data abstraction is utilized in the form of a library of Boolean templates to handle high level descriptions in a commercial hardware description language, VHDL. The correctness of the templates is proved using the Boyer Moore theorem prover before their inclusion in the library.
The hierarchical verification of a simple microprocessor, the Viper, is attempted in this framework. A behavioral description is verified against user-specified properties, including part of the instruction set, and a gate level implementation is proved to correctly implement the behavioral VHDL description.
J. Moondanos, J. A. Wehbeh, J. A. Abraham and D. G. Saab, "VERTEX: VERification of Transistor-level circuits based on model EXtraction," Proceedings The European Conference on Design Automation, Paris, France, February 22-25, 1993, pp. 111-115.
Abstract
This paper describes VERTEX, a program that performs formal verification of synchronous sequential circuits that are described at the transistor-level. Additionally, VERTEX can compare gate-level designs or Boolean specifications against their switch-level implementations. VERTEX verifies a hardware design by employing novel techniques to extract the relevant state variables of a switch-level circuit and to compare the finite state machine descriptions of hardware designs based on formal methods for the verification of sequential circuits.
Y. V. Hoskote, J. Moondanos, J. A. Abraham and D. S. Fussell, "Abstraction of Data Path Registers for Multilevel Verification of Large Circuits," Proceedings Fourth Great Lakes Symposium on VLSI, Univ. of Notre Dame, IN, March 1994, pp. 11-14.
Abstract
Automatic verification of implementations against their specifications in the design hierarchy is largely based on state machine comparison. This paper presents a simple technique that exploits information about correspondence between registers in the data path to enable abstraction of data path registers and make automatic verification of circuits with large data paths tractable. Correspondence between registers which encode the control states is not required. This generality enables efficient verification of large circuits with data paths structured differently, as well as verification against specifications devoid of structural information. Results are presented for the verification of realistic circuits at different levels in the design hierarchy.
Y. V. Hoskote, J. A. Abraham and D. S. Fussell, "Automated verification of temporal properties specified as state machines in VHDL," Proceedings Fifth Great Lakes Symposium on VLSI, Buffalo, NY, March 16-18 1995, pp. 100-105.
Abstract
This paper presents a new verification methodology to prove that a high level HDL description of a synchronous sequential circuit satisfies certain desired behavior or that it is free of certain malicious behavior. The correctness specifications are modeled as state machines with some transitions having unspecified inputs. We show that this suffices for specification of a large class of properties, including both safety and liveliness properties. The properties are described as VHDL programs to enable the designer to simulate them for sample inputs and gain some measure of confidence in their correctness. Experimental results are presented for the Viper microprocessor.
Yatin Hoskote, Jacob Abraham, Donald Fussell and John Moondanos, "Automatic Verification of Implementations of Large Circuits Against HDL Specifications," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 16, March 1997, pp. 217-228.
Abstract
This paper addresses the problem of verifying hte correctness of gate-level implementations of large synchronous sequential circuits with respect to their higher level specifications in a hardware description language (HDL). The verification strategy is to verify containment of the finite-state machine (FSM) represented by the HDL description in the gate-level FSM by computing pairs of compatible states. This formulation of the verification problem dissociates the verification process from the specification of initial states, whose encoding may be unknown or obscured during optimization and also enables verification of reset circuitry. To make verification of large circuits with merger data path and control tractable, the concept of strong containment is introduced. This is a conservative approach which exploits correspondence between data path registers in the two descriptions without requiring any correspondence between the control units. We also present an important results and associated proof that computation of pairs of equivalent or compatible states can be achieved by considering subsets of the circuit outputs. Consequently, verification of circuits with large and diverse input-output sets, which was previously intractable due to lack of a single effective variable order for the binary decision diagrams (BDDs) is now feasible. Experimental results are presented for the verification of several industry level circuits.
Y. Hoskote, D. Moundanos, and J. A. Abraham, "Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors," Proc. IEEE Int'l Conf. on Computer Design, October 1995, pp. 532-537.
Abstract
Simulation is still the primary, although inadequate, resource for verifying the conformity of a design to its functional specifications. Fortunately, most errors in the early stages of design involve only the control flow in the circuit. We define the functional coverage of a given sequence of verification vectors as the amount of control behavior exercised by them. We present a novel technique for automatically extracting the control flow of a design on the basis of the underlying mathematical model. Significantly, this extraction is independent of the circuit description style. The Extracted Control Flow Machine (ECFM) is then used for estimation of functional coverage and to provide information that will help the designer improve the quality of his or her tests.
Integrated Approaches to Test and Verification
The objectives of this research are to develop integrated solutions to the fundamental problems in test and verification and to serve as a conduit of information between research groups in verification and test, further stimulating novel solutions to problems in these two areas. As designs get larger every year, the two major problems faced by the semiconductor industry are to ensure that there are no bugs in the design and that the manufactured chips are defect-free. The program is unique in its emphasis on the application of formal techniques not only to verification, but also to test generation. A key direction of this research is the formulation of powerful abstractions which will reduce the state spaces which need to be searched during verification and test. This project is also developing an integrated set of software tools which will enable digital design engineers to formally verify the correctness of their designs and test the produced chip after manufacture.
Abstract
New approaches to address the difficult problems in test are necessary if its current status as a major bottleneck in the production of quality integrated circuits is to be changed. In this paper we propose a new direction for solving the test problem using powerful methods already employed for the formal verification of large circuits. More specifically, we will discuss how abstraction techniques can assist conventional ATPG tools when attacking hard to detect faults. The same abstractions can also be used in design verification to increase the level of confidence in a design following simulation, by providing a meaningful measure of the coverage achieved by the verification vectors. In this sense, our approach is geared toward providing a unified framework for design validation and manufacturing test.
V. S. S. Nair, K. Indiradevi and J. Abraham, "Formal Checking of Reliable User Interfaces." Fault Tolerant Systems and Software, New Delhi, India, 1996, pp. 17-25.
Abstract
This paper develops techniques for the formal analysis of user interfaces based on a finite-state machine representation. Parameters related to the dependability of an interface can be mapped to desirable properties of the interface, which are themselves represented as finite-state machines. Formal verification tools can then be used to determine whether an interface satisfies desirable properties and to ensure that it does not satisfy undesirable ones. The techniques are illustrated with an example of a simplified Automatic Teller Machine.
Back to:
