• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

A study on debug techniques for digital systems exploiting formal verification methods

Research Project

Project/Area Number 14350178
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field 電子デバイス・機器工学
Research InstitutionThe 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
Project Status Completed (Fiscal Year 2004)
Budget Amount *help
¥14,900,000 (Direct Cost: ¥14,900,000)
Fiscal Year 2004: ¥3,600,000 (Direct Cost: ¥3,600,000)
Fiscal Year 2003: ¥4,300,000 (Direct Cost: ¥4,300,000)
Fiscal Year 2002: ¥7,000,000 (Direct Cost: ¥7,000,000)
KeywordsSystem 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.

Report

(4 results)
  • 2004 Annual Research Report   Final Research Report Summary
  • 2003 Annual Research Report
  • 2002 Annual Research Report
  • Research Products

    (33 results)

All 2005 2004 2003 2002 Other

All Journal Article (25 results) Publications (8 results)

  • [Journal Article] SpecC記述のプログラムスライシングを利用した未初期化変数・未使用変数の検出2005

    • Author(s)
      佐々木俊介, 田辺健, 藤田昌宏
    • Journal Title

      電子情報通信学会技術研究報告 Vol.104,No.708

      Pages: 59-64

    • NAID

      110003318259

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Annual Research Report 2004 Final Research Report Summary
  • [Journal Article] Cベース高位設計における等価性検証フレームワークと反例解析手法の提案2005

    • Author(s)
      松本剛史, 斎藤寛, 藤田昌宏
    • Journal Title

      第18回 回路とシステム軽井沢ワークショップ

      Pages: 557-562

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] On Equivalence Checking Between Behavioral and RTL Descriptions2005

    • Author(s)
      M.Fujita
    • Journal Title

      ACM Transactions on Design Automation of Electornic Systems (掲載予定)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Using SpecC Program Slicing to detect uninitialized variables and unused variables2005

    • Author(s)
      S.Sasaki, K.Tanabe, M.Fujita
    • Journal Title

      Technical Report of IEICE, VLD2004-134

      Pages: 59-64

    • NAID

      110003318259

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Equivalence Checking Framework and Counterexample Analysis Method in C-Based High-Level Design2005

    • Author(s)
      T.Matsumoto, H.Saito, M.Fujita
    • Journal Title

      Proc.of The 18th Workshop on Circuits and Systems in Karuizawa

      Pages: 557-562

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Cベース高位設計における等価性検証フレームワークと反例解析手法の提案2005

    • Author(s)
      松本剛史, 斎藤寛, 藤田昌宏
    • Journal Title

      第18回 回路とシステム軽井沢ワークショップ (発表予定)

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Program Slicing for System Level Designs in SpecC2004

    • Author(s)
      K.Tanabe, S.Sasaki, M.Fujita
    • Journal Title

      Proc. of the IASTED, International Conference on Advances in Computer Science and Technology

      Pages: 252-258

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] A Program Slicing for System Level Description written in SpecC Language2004

    • Author(s)
      K.Tanabe, H.Saito, S.Komatsu, M.Fujita
    • Journal Title

      Technical Report of IEICE, VLD2003-149

      Pages: 79-84

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Program Slicing for System Level Designs in SpecC2004

    • Author(s)
      K.Tanabe, S.Sasaki, M.Fujita
    • Journal Title

      Proc.of the IASTED, International Conference on Advances in Computer Science and Technology

      Pages: 252-258

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Annual Research Report 2004 Final Research Report Summary
  • [Journal Article] Event-Driven Observability Enhanced Coverage Analysis of C Programs for Functional Validation2003

    • Author(s)
      F.Fallah, I.Ghosh, M.Fujita
    • Journal Title

      Proc. Asia South Pacific Design Automation Conference 2003

      Pages: 123-128

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Debug Methodology for Arithmetic Circuits based on Architecture Library Mapping2003

    • Author(s)
      M.Kubo, T.Matsumoto, M.Fujita
    • Journal Title

      Proc. of International Workshop on Logic and Synthesis 2003

      Pages: 73-80

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] SpecC言語によるハードウェア・ソフトウェア混在システム記述を対象としたプログラムスライシング手法の提案2003

    • Author(s)
      田辺 健, 齋藤 寛, 小松 聡, 藤田昌宏
    • Journal Title

      電子情報通信学会技術研究報告 VLSI設計技術 VLD2003-149 103・702

      Pages: 79-84

    • NAID

      110003316386

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Event-Driven Observability Enhanced Coverage Analysis of C Programs for Functional Validation2003

    • Author(s)
      F.Fallah, I.Ghosh, M.Fujita
    • Journal Title

      Proc.Asia South Pacific Design Automation Conference

      Pages: 123-128

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Debug Methodology for Arithmetic Circuits based on Architecture Library Mapping2003

    • Author(s)
      M.Kubo, T.Matsumoto, M.Fujita
    • Journal Title

      Proc.of International Workshop on Logic and Synthesis

      Pages: 73-80

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Verification of Synchronization in SpecC Description with the Use of Difference Decision Diagrams2002

    • Author(s)
      T.Sakunkonchak, M.Fujita
    • Journal Title

      Proc. of Forum on specification & Design Languages (FDL'02) 2002

    • NAID

      110003212601

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] An Equivalence Checking Methodology for Hardware Oriented C-based Specifications2002

    • Author(s)
      H.Saito, T.Ogawa, S.Thanyapat, M.Fujita
    • Journal Title

      Proc. International High Level Design Validation and Test Workshop 2002

      Pages: 139-144

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams2002

    • Author(s)
      T.Sakunkonchak, M.Fujita
    • Journal Title

      Formal Techniques for Networked and Distributed Systems (FORTE2002) 2002

      Pages: 369-369

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Debug Methodology for Arithmetic Circuits on FPGAs2002

    • Author(s)
      Masao Kubo, Masahiro Fujita
    • Journal Title

      In Proc. of IEEE International Conference on Field-Programmable Technology (FPT-02) 2002

      Pages: 236-242

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Coverage Metric for Observability-Based Validation of C Programs2002

    • Author(s)
      F.Fallah, I.Ghosh, M.Fujita
    • Journal Title

      Proc. of Microprocessor Test and Verification (MTV'02) 2002

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Verification of Synchronization in SpecC Description with the Use of Difference Decision Diagrams2002

    • Author(s)
      T.Sakunkonchak, M.Fujita
    • Journal Title

      Proc.of Forum on specification & Design Languages (FDL'02)

    • NAID

      110003212601

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] An Equivalence Checking Methodology for Hardware Oriented C-based Specifications2002

    • Author(s)
      H.Saito, T.Ogawa, S.Thanyapat, M.Fujita
    • Journal Title

      Proc.International High Level Design Validation and Test Workshop

      Pages: 139-144

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams2002

    • Author(s)
      T.Sakunkonchak, M.Fujita
    • Journal Title

      Formal Techniques for Networked and Distributed Systems (FORTE2002)

      Pages: 369-369

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Coverage Metric for Observability-Based Validation of C Programs2002

    • Author(s)
      F.Fallah, I.Ghosh, M.Fujita
    • Journal Title

      Proc.of Microprocessor Test and Verification (MTV'02)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Debug Methodology for Arithmetic Circuits on FPGAs

    • Author(s)
      Masao Kubo, Masahiro Fujita
    • Journal Title

      Proc.of IEEE International Conference on Field-Programmable Technology (FPT-02)

      Pages: 236-242

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] On Equivalence Checking Between Behavioral and RTL Descriptions

    • Author(s)
      M.Fujita
    • Journal Title

      ACM Transactions on Design Automation of Electronic Systems (to be published)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Publications] M.Kubo, T.Matsumoto, M.Fujita: "Debug Methodology for Arithmetic Circuits based on Architecture Library Mapping"Proc.of International Workshop on Logic and Synthesis. 73-80 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 田辺 健, 齋藤 寛, 小松 聡, 藤田 昌宏: "SpecC言語によるハードウェア・ソフトウェア混在システム記述を対象としたプログラムスライシング手法の提案"電子情報通信学会技術研究報告 VLSI設計技術 VLD2003-149. 103・702. 79-84 (2004)

    • Related Report
      2003 Annual Research Report
  • [Publications] Thanyapat Sakunkonchak: "Verification of Synchronization in SpecC Description withthe Use of Difference Decision Diagrams"Proc.of Forum on specification & Design Languages (FDL'02). 2002. (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Hiroshi Saito: "An Equivalence Checking Methodology for Hardware Oriented C-based Specifications"Proc.International High Level Design Validation and Test Workshop. 2002. 139-144 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Thanyapat Sakunkonchak: "Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams"Proc.of Formal Techniques for Networked and Distributed Systems (FORTE2002). 2002. 369 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Masao Kubo: "Debug Methodology for Arithmetic Circuits on FPGAs"Proc.of IEEE International Conference on Field-Programmable Technology(FPT-02). 2002. 236-242 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Farzan Fallah: "Coverage Metric for Observability-Based Validation of C Programs"Proc.of Microprocessor Test and Verification (MTV'02). 2002. (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Farzan Fallah: "Event-Driven Observability Enhanced Coverage Analysis of C Programs for Functional Validation"Proc.Asia South Pacific Design Automation Conference. 2003. 123-128 (2003)

    • Related Report
      2002 Annual Research Report

URL: 

Published: 2002-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi