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

シストリックアレイの形式的検証システムに関する研究

研究課題

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

奨励研究(A)

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

研究代表者

北道 淳司  大阪大学, 基礎工学部, 助手 (20234271)

研究期間 (年度) 1996
研究課題ステータス 完了 (1996年度)
配分額 *注記
900千円 (直接経費: 900千円)
1996年度: 900千円 (直接経費: 900千円)
キーワード同期式順序回路 / 形式的検証 / 代数的手法 / シストリックアレイ / 高位設計 / 仕様記述 / 定理証明
研究概要

研究計画に従い行った研究の概要を述べる.
(1)シストリックアレイの形式的記述法 本研究では,回路仕様記述において回路の大きさをパラメータ付で記述する仕様記述法を提案し,その記述のもとで任意の回路の大きさで,設計の正しさを形式的に定義した.この記述法のもとで,形式的回路検証法のベンチマーク問題の一つである行列の積などを求めるシストリックアレイ回路(Benchmark-Circuits for Hardware-Verification,TPCD94,Vol.901,LN in Computer Science,1995)に対する要求仕様及びその設計を行った.
(2)シストリックアレイの形式的検証
上記(1)で行った設計が正しいことの検証手順を提案し,実際にシステムを用いて検証を行った.検証は,回路の大きさによる帰納法を用いることによって設計されたシストリックアレイ回路が任意の大きさ(入出力データのサイズなど)で要求仕様を満足することを示すことである.帰納法を用いた検証においては,中間補題を考案すること,及び,その中間補題が与えられた実現仕様のもとで成立することを証明することなどの作業ステップからなる.
作成するシステムは,要求仕様,実現仕様,中間補題などからの検証に必要な式の合成機能,その式が恒真であることを証明する定理証明系からなる.合成機能に関しては,必要な補題を設定,自動的な簡約・変形を行う.定理証明系としては,すでに我々の研究グループで開発したルーチン(試験研究05558031など)を利用して作成し,本手法の評価を行った.
本設計法及び検証法に関しては,情報処理学会第52回全国大会にて,システムに関しては1997年春季電子情報通信学会全国大会にて成果発表を行った.

報告書

(1件)
  • 1996 実績報告書
  • 研究成果

    (3件)

すべて その他

すべて 文献書誌 (3件)

  • [文献書誌] 竹中崇: "シストリックアレーによる回路設計の正しさの一証明法" 情報処理学会第52回全国大会論文集. 6分冊. 3-4 (1996)

    • 関連する報告書
      1996 実績報告書
  • [文献書誌] 竹中崇: "代数的手法によるPCIバスコントローラの設計検証" 情報処理学会研究報告. 97-DA-83. 9-16 (1997)

    • 関連する報告書
      1996 実績報告書
  • [文献書誌] 斉藤義勝: "代数的手法を用いた複数の制御部を持つ同期式順序回路に対する設計および検証支援系の開発" 1997年春季電子情報通信学会全国大会論文集. (未発行).

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

URL: 

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

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

Powered by NII kakenhi