• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

ASIC設計の上流工程設計支援システムの開発

研究課題

研究課題/領域番号 05558031
研究種目

試験研究(B)

配分区分補助金
研究分野 計算機科学
研究機関大阪大学

研究代表者

谷口 健一  大阪大学, 基礎工学部, 教授 (00029513)

研究分担者 杉山 裕二  岡山大学, 工学部, 教授 (50116050)
岡野 浩三  大阪大学, 基礎工学部, 助手 (70252632)
北道 淳司  大阪大学, 基礎工学部, 助手 (20234271)
松浦 敏雄 (松浦 敏夫)  大阪大学, 情報処理教育センター, 助教授 (40127296)
東野 輝夫  大阪大学, 基礎工学部, 助教授 (80173144)
研究期間 (年度) 1993 – 1994
研究課題ステータス 完了 (1994年度)
配分額 *注記
3,900千円 (直接経費: 3,900千円)
1994年度: 1,100千円 (直接経費: 1,100千円)
1993年度: 2,800千円 (直接経費: 2,800千円)
キーワード同期式順序回路 / 代数的手法 / ASIC / 段階的詳細化 / 設計検証 / CAD / プレスブルガ-文 / 状態図変形 / 高位合成 / グラフィカルユーザインタフェース / 機能設計 / 形式的手法 / 設計自動化
研究概要

ASIC(Application Specific IC)開発において,アーキテクチャ決定などの上流工程での設計では,設計の正しさの保証,設計における自動化可能なステップの自動化等が重要な課題である.本研究では,ASIC開発における,代数的言語を用いた同期式順序回路の記述法,要求記述からの段階的設計法,設計の正しさの検証法,回路性能の向上のための状態図変換法を考案し,それらの方法に基づく設計支援システムを実現した.
(1)要求仕様を記述するレベルでは,各抽象レジスタが抽象的な一動作の実行の前後でどのような関係を満たすかを記述する.要求仕様から,用いる動作アルゴリズム,アーキテクチャ,部品の機能などを順次決定しながら段階的に回路を設計し,論理設計レベルの記述を得る.
(2)各段階の設計の正しさを形式的に検証するための検証支援系を作成した.この支援系には,全称記号∀のみの冠頭標準形プレスブルガ-文の高速な真偽判定ルーチンを実現しており,検証者が不変表明や用いる述語に関する補題(定理)を与えれば,自動的に検証を行うことができる.
(3)上記の方法により得られた回路の性能向上のための状態図変形支援系を作成した.一般に,設計者が最適化のため一度に大幅な変形を行うと等価性を保証するのが難しいので,回路の等価性を保存する比較的簡単な状態図変形ルールを繰返し適用し,回路の最適化を行う.各ルールの適用条件の判定は検証支援系を利用する.
(4)得られた論理設計レベルの記述を回路記述言語SFLに変換する機能を作成した.以降の回路設計は,NTTが開発した回路自動合成系パルテノンシステムを用いて行うことができる.
(5)CPUやソ-ト回路を例題に用いて,本手法や支援システムの有効性の評価を行った.

報告書

(3件)
  • 1994 実績報告書   研究成果報告書概要
  • 1993 実績報告書
  • 研究成果

    (29件)

すべて その他

すべて 文献書誌 (29件)

  • [文献書誌] Junji Kitamichi, Sumio Morioka, Teruo Higashino and Kenichi Taniguchi: ""Automatic Correctness Proof of Implementation of Synchronous Sequential Circuits Using Algebraic Approach"" Proceedings of the Second International Conference on Theorem Provers in Circuit Design(TPCD'94),Lecture Notes in Computer Science,Springer Verlag,. 901. 165-184 (1994)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 北道淳司,東野輝夫,谷口健一,杉山裕二: ""代数的手法を用いた同期式順序回路の段階的設計法"" 電子情報通信学会論文誌(A). J77-ANo.3. 420-429 (1994)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 谷口健一,北道淳司: ""代数的手法による仕様記述と設計及び検証"" 情報処理. Vol.35No.8. 742-750 (1994)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 谷口健一,北道淳司: ""代数的手法を用いた仕様記述と設計及び検証"" 第6回回路とシステム軽井沢ワークショップ論文集. 375-380 (1993)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 森岡澄夫,北道淳司,東野輝夫,谷口健一: ""同期式順序回路の設計検証例"" DAシンポジウム'93論文集,. 73-76 (1993)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 森岡澄夫,北道淳司,東野輝夫,谷口健一: ""代数的手法を用いた順序回路の段階的設計支援システムにおける状態図変形機能"" 第8回回路とシステム軽井沢ワークショップ(発表予定). (1995)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 森岡澄夫,北道淳司,東野輝夫,谷口健一: ""整数上の論理式の恒真性判定アルゴリズムを用いた組合せ論理回路の実現の正しさの証明"" 情報処理学会第49回全国大会(4L-01). Vol.6. 87-88 (1994)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 北嶋暁,森岡澄夫,北道淳司,東野輝夫,谷口健一: ""代数的言語ASLによる回路設計支援システムにおけるAFL記述への詳細化とその変更およびそれらの正しさの検証"" 情報処理学会第49回全国大会(4L-07). Vol.6. 99-100 (1994)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 村上尚,北道淳司,森岡澄夫,西川清史,谷口健一: ""代数的手法を用いた同期式順序回路の設計支援機能の統合"" 1995年電子情報通信学会春期大会(A121). 基礎/境界. 121- (1995)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Junji Kitamichi, Sumio Morioka, Teruo Higashino and Kenichi Taniguchi: ""Automatic Correctness Proof of Implementation of Synchronous Sequential Circuits Using Algebraic Approach"" Proceedings of the Second International Conference on Theorem Provers in Circuit Design (TPCD'94) , Lecture Notes in Computer Science, Springer Verlag. Vol.901. 165-184 (1994)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Junji Kitamichi, Teruo Higashino, Kenichi Taniguchi, Yuji Sugiyama: ""Top-Down Design Method for Synchronous Sequential Logic Circuits Based on Algebraic Technique"" Transactions of the IEICE Japan. J77A,No.3. 420-429 (1994)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Kenichi Taniguchi and Junji Kitamichi: ""Design and Verification of Sequential Logic Circuits Based on Algebraic Technique"" Transactions of the Information Processing Japan. Vol.35No.8. 742-750 (1994)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Kenichi Taniguchi and Junji Kitamichi: ""Specification, Refinement and Verification based on Algebraic Method"" Proceedings of the 6th Karuizawa Workshop on Circuits and Systems. 375-380 (1993)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Sumio Morioka, Junji Kitamichi, Higasino Teruo and Kenichi Taniguchi: ""Examples of Design Verification of Synchronous Logic Circuit based on Algebraic Method"" Proceedings of the DA Symposium93'. Vol.35No.8. (1993)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Sumio Morioka, Junji Kitamichi, Higasino Teruo and Kenichi Taniguchi: ""Facilities for State Diagran Transformation in Hardware Design Support System based on Algebraic Method"" Proceedings of the 8th Karuizawa Workshop on Circuits and Systems. (1995)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Sumio Morioka, Junji Kitamichi, Higasino Teruo and Kenichi Taniguchi: ""Example of Correctness Proof of the Implementation of Combinatorial Logic Circuits Using Presburger Arithmetic Decision Procedure"" Proceedings of the 49th General Conference, Information Processing Society of Japan, (4L-01). Vol.6. 87-88 (1994)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Akira Kitajima, Sumio Morioka, Junji Kitamichi, Higasino Teruo and Kenichi Taniguchi: ""Refinement of Sequential Circuits to SFL Descriptions and Re-design with Verifications of Design Correctness Using a Circuit Design Support System based on Algebraic Method"" Proceedings of the 49th General Conference, Information Processing Society of Japan, (4L-07). Vol.6. 99-100 (1994)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] Takashi Murakami, Junji Kitamichi, Sumio Morioka, Seishi Nishikawa and Kenichi Taniguchi: ""Development of Design Support System using GUI for Synchronous Circuits with Algebraic Method"" Proceedings of the 1995 IEICE General Conference. Vol.1. 121 (1995)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1994 研究成果報告書概要
  • [文献書誌] 谷口健一: "代数的手法による仕様記述と設計及び検証" 情報処理. Vol.35No.8. 742-750 (1994)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 東野輝夫: "Hardware Synthesis from a Restricted Class of LOTOS Expressions" Proceedings of the 14th International Symposium on protocol Specification,Testing,and Verification(PSTV-XIV). 379-386 (1994)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 北道淳司: "Automatic Correctness Proof of Implementation of Synchronous Sequential Circuits Using Algebraic Approach" 2nd International Conference on Theorem Provers in Circuit Design(TPCD94). (1994)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 森岡澄夫: "代数的手法を用いた順序回路の段階的設計支援システムにおける状態図変形機能" 第8回 回路とシステム軽井沢ワークショップ. (1995)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 森岡澄夫: "整数上の論理式の恒真性判定アルゴリズムを用いた組合せ論理回路の実現の正さの証明" 第49情報処理全国大会回講演論文集. 4L-01. 6‐87-6‐88 (1994)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 北嶋暁: "代数的言語ASLによる回路設計支援システムにおけるSFL記述への詳細化とその変更およびそれらの正しさの検証" 第49情報処理全国大会回講演論文集. 4L-07. 6‐99-6‐100 (1994)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 村上尚: "代数的手法を用いた同期式順序回路の設計支援機能の統合" 1995年春期信学全大. A121. (1995)

    • 関連する報告書
      1994 実績報告書
  • [文献書誌] 北道 淳司: "代数的手法を用いた同期式順序回路の方式・機能設計と検証例" 1993年秋期電子情報通信学会全国大会. Vol.1. 276-277 (1993)

    • 関連する報告書
      1993 実績報告書
  • [文献書誌] 谷口健一: "代数的手法を用いた仕様記述と設計及び検証" 回路とシステム軽井沢ワークショップ論文集. 375-380 (1993)

    • 関連する報告書
      1993 実績報告書
  • [文献書誌] 北道淳司: "代数的手法を用いた同期式順序回路の段階的設計法" 電子情報通信学会論文誌(A分冊). No.3(採録決定). (1993)

    • 関連する報告書
      1993 実績報告書
  • [文献書誌] 森岡澄夫: "同期式順序回路の設計検証例" 情報処理DAシンポジウム'93論文集. 73-76 (1993)

    • 関連する報告書
      1993 実績報告書

URL: 

公開日: 1993-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi