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

Hardware Verification with respect to Program Specification

Research Project

Project/Area Number 14580377
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionWaseda University

Principal Investigator

KIMURA Shinji  Waseda University, Graduate School of Information, Production and Systems, Professor, 情報生産システム研究科, 教授 (20183303)

Project Period (FY) 2002 – 2004
Project Status Completed (Fiscal Year 2004)
Budget Amount *help
¥2,900,000 (Direct Cost: ¥2,900,000)
Fiscal Year 2004: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2003: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2002: ¥1,500,000 (Direct Cost: ¥1,500,000)
KeywordsHigh-level Design Verification / C based Hardware Design / Reconfigurable Hardware / Verification of Arithmetic Circuits / Equivalence Verification / Uninterpreted Function / 設計検証 / 高位検証 / 再構成可能素子の検証 / テクノロジーマッピング検証 / 映像処理向け検証 / 再構成可能アーキテクチャ検証 / マルチメディア処理向け検証 / 無評価関数 / Cプログラム検証
Research Abstract

With the recent development of integrated circuit technology, we can integrate 1 million transistors in one chip. For the design of such huge circuits, high-level design methodologies have been developed and applied to many application specific chips. In the high-level design, programming languages are used to describe the functionality and the description is automatically converted to hardware modules based on high-level synthesis algorithms. So the modification and verification should be done at programming level and high-level verification methods are needed. In this research, we have developed several basic algorithms to show the correctness of hardware modules with respect to the program specification.
At first, we have surveyed the current research on the equality with uninterpreted function and its application to software and hardware verification. We have also checked the current equality systems such as SVC, CLVL, etc. We have applied these systems for the verification of arith … More metic circuits and shown the limitation of such systems. We have also applied the equality checking systems for the verification of parallel and pipeline circuits.
In the equality checking, the algorithm uses logic formulae to represent and decide the equality. For the acceleration of the decision procedure, we proposed a prototyping system based on new look-up-table architecture of Field Programmable Gate Array. We have devised the architecture and proposed a mapping method for the new architecture. The architecture is more area-efficient and faster compared to the usual loop-up-table architecture.
For the program specification, we have proposed a control-data-flow graph based data-path optimization methods. Especially, we focused on the bit-width of data-paths and proposed an optimization method of integer operations and an error estimation method for floating point operations. With the optimization and estimation algorithms, we can verify application specific circuits written in C programs.
We have also worked on the high-level test and proposed a test pattern compaction method with small area overhead for system-on-chip design. Less

Report

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

    (28 results)

All 2005 2004 2003 2002 Other

All Journal Article (18 results) Publications (10 results)

  • [Journal Article] 非線形計画法と整数解の探索に基づく高位合成向けビット長最適化2005

    • Author(s)
      土井伸洋, 堀山貴志, 中西正樹, 木村晋二
    • Journal Title

      情報処理学会システムLSI設計技術研究会報告

      Pages: 1-6

    • Related Report
      2004 Annual Research Report
  • [Journal Article] A Hybrid Dictionary Test Data Compression for Multiscan-based Designs2004

    • Author(s)
      Y.Shi, S.Kimura, M.Yanagisawa, T.Ohtsuki
    • Journal Title

      IEICE Trans.Fundamentals E87-A, No.12

      Pages: 3193-3199

    • NAID

      110003212857

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] A Hybrid Dictionary Test Data Compression for Multiscan-based Designs2004

    • Author(s)
      Y.Shi, S.Kimura, M.Yanagisawa, T.Ohtsuki
    • Journal Title

      IEICE Trans.Fundamentals Vol.E87-A, No.12

      Pages: 3193-3199

    • NAID

      110003212857

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] A Hybrid Dictionary Test Data Compression for Multiscan-based Designs2004

    • Author(s)
      Y.Shi, S.Kimura, M.Yanagisawa, T.Ohtsuki
    • Journal Title

      IEICE Trans. Fundamentals E87-A, No.12

      Pages: 3193-3199

    • NAID

      110003212857

    • Related Report
      2004 Annual Research Report
  • [Journal Article] A Selective Scan Chain Reconfiguration through Run-Length Coding for Test Data Compression and Scan Power Reduction2004

    • Author(s)
      Y.Shi, S.Kimura, M.Yanagisawa, T.Ohtsuki
    • Journal Title

      IEICE Trans.Fundamentals E87-A, No.12

      Pages: 3208-3215

    • NAID

      110003212859

    • Related Report
      2004 Annual Research Report
  • [Journal Article] An Optimization Method in Floating-point to Fixed-point Conversion using Positive and Negative Error Analysis and Sharing of Operations2004

    • Author(s)
      N.Doi, T.Horiyama, M.Nakanishi, S.Kimura
    • Journal Title

      Proc.of Workshop on Synthesis and System Integration of Mixed Technologies (SASIMI'2004)

      Pages: 466-471

    • Related Report
      2004 Annual Research Report
  • [Journal Article] 浮動小数点演算での誤差の増減を考慮した変数ビット長の最適化2004

    • Author(s)
      土井伸洋, 堀山貴史, 中西正樹, 木村晋二
    • Journal Title

      DAシンポジウム2004論文集

      Pages: 85-90

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Reconfigurable Architecture for Bit-Level Data Processing2004

    • Author(s)
      S.Kimura
    • Journal Title

      Proceedings of 1st Silicon-Seabelt Workshop on VLSI Designs

      Pages: 1-6

    • Related Report
      2004 Annual Research Report
  • [Journal Article] A Built-in Reseeding Technique for LFSR-Based Test Pattern Generation2003

    • Author(s)
      Y.Shi, Z.Zhang, S.Kimura, M.Yanagisawa, T.Ohtsuki
    • Journal Title

      IEICE Trans.Fundamentals E86-A, No.12

      Pages: 3056-3662

    • NAID

      110003212586

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Bit Length Optimization of Fractional Part on Floating to Fixed Point Conversion for High Level Synthesis2003

    • Author(s)
      N.Doi, T.Horiyama, N.Nakanishi, S.Kimura, K.Watanabe
    • Journal Title

      IEICE Trans.Fundamentals E86-A, No.12

      Pages: 3176-3183

    • NAID

      110003212600

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] An On-Chip High Speed Serial Communication Method Based on Independent Ring Oscillators2003

    • Author(s)
      S.Kimura, T.Hayakawa, T.Horiyama, M.Nakanishi, K.Watanabe
    • Journal Title

      Proc.of International Solid State Circuit Conference

      Pages: 390-391

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] A Built-in Reseeding Technique for LFSR-Based Test Pattern Generation2003

    • Author(s)
      Y.Shi, Z.Zhang, S.Kimura, M.Yanagisawa, T.Ohtsuki
    • Journal Title

      IEICE Trans.Fundamentals Vol.E86-A, No.12

      Pages: 3056-3662

    • NAID

      110003212586

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Bit Length Optimization of Fractional Part on Floating to Fixed Point Conversion for High Level Synthesis2003

    • Author(s)
      N.Doi, T.Horiyama, N.Nakanishi, S.Kimura, K.Watanabe
    • Journal Title

      IEICE Trans.Fundamentals Vol.E86-A, No.12

      Pages: 3176-3183

    • NAID

      110003212600

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] An On-Chip High Speed Serial Communication Method Based on Independent Ring Oscillators2003

    • Author(s)
      S.Kimura, T.Hayakawa, T.Horiyama, M.Nakanishi, K.Watanabe
    • Journal Title

      Proc.of International Solid State Circuit Conference 03 22.3

      Pages: 390-391

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Bit Length Optimization of Fractional Parts on Floating to Fixed Point Conversion for High-Level Synthesis2003

    • Author(s)
      N.Doi, T.Horiyama, M.Nakanishi, S.Kimura, K.Watanabe
    • Journal Title

      Workshop on Synthesis and System Integration of Mixed Technologies (SASIMI'2003)

      Pages: 129-136

    • NAID

      110003212600

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Look Up Table Compaction Based on Folding of Logic Functions2002

    • Author(s)
      S.Kimura, A.Ishii, T.Horiyama, M.Nakanishi, H.Kajihara, K.Watanabe
    • Journal Title

      IEICE Trans.Fundamentals E85-A, No.12

      Pages: 2701-2707

    • NAID

      110003212441

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Folding of Logic Functions and Its Application to Look Up Table Compaction2002

    • Author(s)
      S.Kimura, T.Horiyama, M.Nakanishi, H.Kajihara
    • Journal Title

      Proc.on ICCAD 2002 (International Conference on Computer Aided Design)

      Pages: 694-697

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Look Up Table Compaction Based on Folding of Logic Functions2002

    • Author(s)
      S.Kimura, A.Ishii, T.Horiyama, M.Nakanishi, H.Kajihara, K.Watanabe
    • Journal Title

      IEICE Trans.Fundamentals Vol.E85-A, No.12

      Pages: 2701-2707

    • NAID

      110003212441

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Publications] N.Doi, T.Horiyama, N.Nakanishi, S.Kimura, K.Watanabe: "Bit Length Optimization of Fractional Part on Floating to Fixed Point Conversion for High Level Synthesis"IEICE Trans.Fundamentals. Vol.E86-A, No.12. 3176-3183 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Y.Shi, Z.Zhang, S.Kimura, M.Yanagisawa, T.Ohtsuki: "A Built-in Reseeding Technique for LFSR-Based Test Pattern Generation"IEICE Trans.Fundamentals. Vol.E86-A, No.12. 3056-3662 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 清水友樹, 木村晋二, 堀山貴史, 中西正樹, 柳澤政生: "畳み込み機構を持つFPGAのマッピング能力について"DAシンポジウム2003論文集. 31-36 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 原田恭典, 木村晋二, 柳澤政生: "プロセッサにおける配線の再構成可能性の利用について"情報処理学会研究報告. 2004-SLDM-113. 1-6 (2004)

    • Related Report
      2003 Annual Research Report
  • [Publications] S.Kimura, A.Ishii, T.Horiyama, M.Nakanishi, H.Kajihara, K.Watanabe: "Look Up Table Compaction Based on Folding of Logic Functions"IEICE Trans. Fundamentals. E85-A・12. 2701-2707 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] S.Kimura, T.Horiyama, M.Nakanishi, H.Kajihara: "Folding of Logic Functions and Its Application to Look Up Table Compaction"Proc. of ICCAD 2002. 694-697 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 中村, 中西, 堀山, 鈴木, 木村, 渡邉: "環境適応可能なリアルタイム視線推定LSIの設計と評価"第15回 回路とシステム(軽井沢)ワークショップ. 293-298 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 梶原, 早川, 松本, 森下, 鈴木, 中西, 堀山, 木村, 渡邉: "肌色判定と顔の対称性を利用した対顔判定LSI"第15回 回路とシステム(軽井沢)ワークショップ. 529-534 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 土井, 堀山, 中西, 木村, 渡邉: "浮動小数点を含むCプログラムからのハードウェア生成におけるビット長最適化"DAシンポジウム2002 論文集. 119-124 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 梶原, 中西, 堀山, 木村, 渡邉: "論理関数の畳み込みを導入した省面積FPGAの実現"電子情報通信学会 信学技報. 37-42 (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