Abstract/Details

An infrastructure for RTL validation and verification


2002 2002

Other formats: Order a copy

Abstract (summary)

With the increase in size and complexity of digital designs, it has become imperative to address critical validation and verification issues at early stages of the design cycle. This requires robust, automated verification tools at higher (behavioural or register-transfer) level of abstraction. This dissertation describes tools and techniques to assist validation and symbolic verification of high-level or RTL descriptions of digital designs. In particular, a comprehensive infrastructure has been developed that assists in: (i) validation of the descriptions via simulation, and (ii) their functional equivalence verification. A prototype system has been developed around a hardware description language compiler in order to automate the process of validation and verification of RTL descriptions.

The validation part of the infrastructure consists of Satisfiability (SAT) solvers based on Binary Decision Diagrams (BDD) that have been developed to automatically generate functional vectors to simulate the design. BDD-based SAT solvers suffer from the memory explosion problem. To overcome this limitation, two SAT solvers have been developed that employ the elements of the unate recursive paradigm to control the growth of BDD-size while quickly searching for solutions. Experiments carried out over a wide range of designs—ranging from random Boolean logic to regular array structures such as multipliers and shifters—demonstrate the robustness of these techniques.

The verification part of the framework consists of equivalence checking tools that can verify the equivalence of RTL descriptions of digital designs. RTL descriptions represent high-level computations in abstract, symbolic forms from which low-level (binary) details are difficult to extract; the implementation details of logic blocks are not always available. Contemporary canonic representations do not have the scalability or the versatility to efficiently represent RTL descriptions in compact form. For this reason, a new representation called Taylor Expansion Diagrams (TED) has been developed to assist in functional equivalence verification of high-level descriptions of digital designs.

TEDs are a compact, canonical, graph-based representation that are based upon a general non-binary decomposition principle using the Taylor series expansion. RTL computations are viewed as polynomials of a finite degree and TEDs are constructed for them. A set of reduction rules are applied to the diagram to make it canonical. TEDs also have the power to represent word-level algebraic computations in abstract symbolic form that allows to efficiently solve the equivalence checking problem for digital designs. The theoretical fundamentals behind TEDs are discussed and their efficient implementation is described. The robustness of the TED representation is analyzed by carrying out equivalence verification experiments over both equivalent and non-equivalent designs. It is shown that TEDs are exceptionally suitable for verifying large designs that contain not only algebraic (arithmetic) datapaths, but also model their interaction with Boolean variables.

Indexing (details)


Subject
Electrical engineering;
Computer science
Classification
0544: Electrical engineering
0984: Computer science
Identifier / keyword
Applied sciences, Canonic representations, Equivalence verification, Register-transfer language
Title
An infrastructure for RTL validation and verification
Author
Kalla, Priyank
Number of pages
125
Publication year
2002
Degree date
2002
School code
0118
Source
DAI-B 63/10, Dissertation Abstracts International
Place of publication
Ann Arbor
Country of publication
United States
ISBN
9780493880518, 0493880518
Advisor
Ciesielski, Maciej
University/institution
University of Massachusetts Amherst
University location
United States -- Massachusetts
Degree
Ph.D.
Source type
Dissertations & Theses
Language
English
Document type
Dissertation/Thesis
Dissertation/thesis number
3068570
ProQuest document ID
305594361
Copyright
Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works.
Document URL
http://search.proquest.com/docview/305594361
Access the complete full text

You can get the full text of this document if it is part of your institution's ProQuest subscription.

Try one of the following:

  • Connect to ProQuest through your library network and search for the document from there.
  • Request the document from your library.
  • Go to the ProQuest login page and enter a ProQuest or My Research username / password.