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)

Electrical engineering;
Computer science
0544: Electrical engineering
0984: Computer science
Identifier / keyword
Applied sciences; Canonic representations; Equivalence verification; Register-transfer language
An infrastructure for RTL validation and verification
Kalla, Priyank
Number of pages
Publication year
Degree date
School code
DAI-B 63/10, Dissertation Abstracts International
Place of publication
Ann Arbor
Country of publication
United States
9780493880518, 0493880518
Ciesielski, Maciej
University of Massachusetts Amherst
University location
United States -- Massachusetts
Source type
Dissertations & Theses
Document type
Dissertation/thesis number
ProQuest document ID
Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works.
Document URL
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.