2004 Fiscal Year Final Research Report Summary
A study on debug techniques for digital systems exploiting formal verification methods
| Project/Area Number |
14350178
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
電子デバイス・機器工学
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
FUJITA Masahiro The University of Tokyo, VLSI Design and Education Center, Professor, 大規模集積システム設計教育研究センター, 教授 (70323524)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KOMATSU Satoshi The University of Tokyo, VLSI Design and Education Center, Research Associate, 大規模集積システム設計教育研究センター, 助手 (90334325)
|
|---|
| Project Period (FY) |
2002 – 2004
|
| Keywords | System LSI / Formal Verification / Debug / Design Analysis / Equivalence Verification / Model Checking / System-Level Design / Arithmetic Unit |
|---|
| Research Abstract |
As advanced process and device technologies have realized System-on-Chip, in which whole system is integrated, many techniques related to SoC have been studied. Computer Aided Design (CAD) has also become indispensable for SoC designs to reduce the design period and to guarantee the correctness of the design.
In this study, we have studied on the debug flow and debug techniques of very large scale digital systems by exploiting formal verification techniques for the analysis of the designs when the analysis is required because of faults of designs or modification of the specification. In the conventional studies, register transfer level (RTL) designs were handled for the design language. In this study, however, we have handled not only RTL designs but also system level designs in which hardware and software of the digital systems are mixed. Therefore, the consistent debug framework from specification level has been established.
We have studied in terms of the following aspects to establish the debug framework for very large scale digital systems.
(1)Program slicing technique for system level designs and its application for system verification
(2)Property verification method with abstraction refinement for system level designs
(3)Equivalence verification method for hardware oriented C-based designs.
(4)Debug methodology for arithmetic circuits
(1), (2), and (3) are the techniques for high level design and they analyze or debug the whole system on the assumption that all functional units, such as arithmetic units, are correct circuits. (4) is the technique which debugs the arithmetic units independently.
Throughout the study, the above techniques have been established. By using those techniques together, we believe that the time spent for not only debug but also whole system LSI design can be reduced. In addition, we believe those techniques also enable the system LSIs which thoroughly utilize enormous transistor resources in the future semiconductor technology.
|
Research Products
(24 results)
