Enhanced Formal Checkers for RTL Circuit Designs

Orchid DIT-PRJ-04-015

Status NOT active project
DISI role Partner
Project type Research Project
Dimension Trentino
Acquisition date 2004-07-09
Start date 2004-09-30
End date 2007-09-30

Project details

Project astract Formal methods are widely applied as powerful verification and early debugging techniques in the development of complex industrial systems. In particular, formal checking at Register-Transfer Level (RTL) is currently a fundamental step in the design of hardware circuits. A number of techniques and tools have been developed, able to carry out equivalence checking and property checking of combinational and sequential circuits. Historically, Binary Decision Diagrams (BDDs) [10] provide the core technology for formal equivalence and property checking [32, 11, 2]. In the past few years, propositional satisfiability (SAT) techniques have been increasingly accepted as complementary to BDD-based techniques both in equivalence checking [30], and in property checking [3, 8, 1, 43]. Major advantages of SAT-based over BDD-based model checking are the ability to analyze larger designs, and the limited need of tuning to achieve efficiency, that results in enhanced usability by non-expert users and increased productivity. Most tools for formal checking, however, work at the boolean level, which is not expressive enough to capture the abstract, high level (e.g., structural, word level) information of RTL designs. Tools for formal checking are thus confronted with problems which are flattened down to boolean level so that a predominant part of their computational effort is wasted due to the loss of the high-level information that has been compiled away. For example, consider the case of an ALU block in two different circuits being compared: a huge amounts of CPU time and memory is wasted in performing useless boolean search on the bitwise encoding of integer data and arithmetical operations. Thus, the checking process would greatly benefit from the ability to represent and exploit higher level information, thus reducing the need for brute force reasoning on the flattened subproblems. The goal of this project is to investigate enhanced SAT-based techniques for RTL formal checking and to deliver better verification tools for RTL designs. These tools will avoid flattening by working directly at a level of expressivity higher than boolean reasoning, and will be able to analyze larger scale RTL designs. The results of the research will be applicable to the extension of any existing formal checkers based on SAT procedures. Furthermore, the project will thoroughly investigate the customization of hybrid satisfiability techniques to a wide classes of formal checkers (equivalence checking and property checking, oriented to debugging and to verification, incomplete and complete techniques). Collaboration and joint research activity, on the project-related topics, with internationally renowned research and/or industrial institutions, will be pursued. In particular, preliminary contacts have been set up with the Logic and Validation Technologies, Intel Architecture Group of Haifa, Israel (INTEL henceforth). Particular care will be devoted to technology transfer, dissemination, cross-fertilization, and training. Exploitation of the results will be pursued also in different domains other than RTL design verification.
Keywords formal verification, RTL designs
Fundings 440305 €
Partners
  • ITC-Irst, SRA Division
  • DIT
  • ITC-Irst

DISI Sub-project details

Project astract same as project description
Fundings 171883 €
Manager Roberto Sebastiani