An infrastructure for RTL validation and verification

• Main Author: Kalla, Priyank
• Language: ENG
• Published: ScholarWorks@UMass Amherst 2002
• Subjects: Electrical engineering|Computer science
• Online Access: https://scholarworks.umass.edu/dissertations/AAI3068570

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.