関数型言語系とグリッド環境上のプルーフチェッカを融合した超並列演算器の設計検証法

2010 年度 研究成果報告書

• 研究課題/領域番号: 20500130
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 知能情報学
• 研究機関: 信州大学
• 研究代表者: 和崎 克己 信州大学, 工学部, 教授 (70271492)
• 研究期間 (年度): 2008 – 2010
• キーワード: 探索・論理・推論アルゴリズム / プルーフチェッカ

研究概要

プルーフチェッカ(Proof Checker)を,ネットワーク環境上へ実装し,並列システムの検証能力の向上を図る.対象回路の構成情報は,関数型言語系の上で記述し,コンパイラ出力として,プルーフチェッカへの証明式の列を得る.並列性実現のため「パイプライン機構」を説明する計算モデルとして,ペトリネット表現モデルを導入した.次に,関数型言語系上のハードウェアコンパイラを開発した.更に検証済み演算器の形式検証を実施した.

研究成果

• [雑誌論文] Quantum Circuits, Lots, Interference and Basis of Neuro-Computations (2009)
  • 著者名/発表者名: Hiroyuki MATSUURA, Masahiro NAKANO, Katsumi WASAKI
  • 雑誌名: ICIC Express Letters, ICIC International 3,(1) ページ: 7-14
  • 査読あり
• [雑誌論文] A Meta Hardware Description Language Melasy for Model-Checking Systems (2008)
  • 著者名/発表者名: Naoki IWASAKI, Katsumi WASAKI
  • 雑誌名: Proceedings of the 5th International Conference on Information Technology : New Generations (ITNG2008) ページ: 273-278
  • 査読あり
• [雑誌論文] Correctness of the Stability of the 4-2 Compressor Cell for Partial Product Reduction in Parallel Multiplier Circuits (2008)
  • 著者名/発表者名: Katsumi WASAKI
  • 雑誌名: Mechanized Mathematics and Its Applications 7,(2) ページ: 17-25
  • 査読あり
• [雑誌論文] Stability of the 4-2 Binary Addition Circuit Cells.Part I (2008)
  • 著者名/発表者名: Katsumi WASAKI
  • 雑誌名: Formalized Mathematics 16,(4) ページ: 377-387
  • 査読あり
• [雑誌論文] Stability of n-Bit Generalized Full Adder Circuits (GFAs). Part II (2008)
  • 著者名/発表者名: Katsumi WASAKI
  • 雑誌名: Formalized Mathematics 16,(1) ページ: 73-80
  • 査読あり
• [学会発表] Automatic Code Generation and Integrated Testing for Model Checking and Hardware Implementation using A Meta Description Language : Melasy+ (2010)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: 平成22年度IEEE信越支部セッション講演論文集,(11B-4),206
  • 発表場所: 長岡技術科学大学
  • 年月日: 2010-10-02
• [学会発表] Upper Scalable Modeling of The Stream Processing Architecture by using A Specification Language : LOTOS (2010)
  • 著者名/発表者名: Pratima K.SHAH, Katsumi WASAKI
  • 学会等名: 平成22年度IEEE信越支部セッション講演論文集,(11B-2),204
  • 発表場所: 長岡技術科学大学
  • 年月日: 2010-10-02
• [学会発表] 上位ハードウェア設計言語Melasy+によるVHDLコード生成と動作検証 (2010)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: FIT2010(第9回情報科学技術フォーラム)講演論文集,1,(C-002),371-374
  • 発表場所: 九州大学伊都キヤンハス
  • 年月日: 2010-09-08
• [学会発表] 上位言語Melasy+による自己テスト機能付バスアービタの設計とNuSMVを用いた検証 (2010)
  • 著者名/発表者名: 花里貴裕, 白鳥航亮, 和崎克己
  • 学会等名: 情報処理学会第72回全国大会講演論文集,1,(1M-4),151-152
  • 発表場所: 東京大学本郷キャンパス
  • 年月日: 2010-03-10
• [学会発表] 上位ハードウェア記述言語Melasy+に対する仕様パターン埋め込みと展開 (2010)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: 情報処理学会第72回全国大会講演論文集,1,(1M-3),149-150
  • 発表場所: 東京大学本郷キャンパス
  • 年月日: 2010-03-10
• [学会発表] 時間ペトリネットを用いた非同期論理ゲートのモデルと階層化同路合成 (2009)
  • 著者名/発表者名: 松山千尋, 和崎克己
  • 学会等名: 平成21年度電子情報通信学会信越支部大会講演論文集,(2D-3),38
  • 発表場所: 信州大学長野(工学)キャンパス
  • 年月日: 2009-10-03
• [学会発表] HDCamlハードウェア上位記述に対するLOTOSコード生成系について (2009)
  • 著者名/発表者名: 桑島芳朗, 和崎克己
  • 学会等名: 平成21年度電子情報通信学会信越支部大会講演論文集,(2B-4),29
  • 発表場所: 信州大学長野(工学)キャンパス
  • 年月日: 2009-10-03
• [学会発表] 上位記述言語Melasy+を用いたセル型FIFOメモリの自己同復性の検証 (2009)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: 平成21年度電子情報通信学会信越支部大会講演論文集,(2B-3),28
  • 発表場所: 信州大学長野(工学)キャンパス
  • 年月日: 2009-10-03
• [学会発表] Time-Petri Netを用いた非同期同路のモデル化と階層化設計 (2009)
  • 著者名/発表者名: 松山千尋, 和崎克己
  • 学会等名: FIT2009(第8回情報科学技術フォーラム)講演論文集,1,(C-038),523-526
  • 発表場所: 東北工業大学八木山キャンパス
  • 年月日: 2009-09-04
• [学会発表] 上位ハードウェア設計言語Melasy+による自己回復機能付きFIFOメモリの記述と検証 (2009)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: FIT2009(第8回情報科学技術フォーラム)講演論文集,1,(C-011),451-454
  • 発表場所: 東北工業大学八木山キャンパス
  • 年月日: 2009-09-03
• [学会発表] 整数有限列上の加算・乗算アルゴリズムの正当性証明に関する検討 (2009)
  • 著者名/発表者名: 伊藤比佐志, 和崎克己
  • 学会等名: 日本Mizar学会2009年春期総会予稿集(Proceedings of the Technical Symposium and General Assembly of Mizar JAPAN),4,(1),6pages
  • 発表場所: 信州大学長野(工学)キャンパス総合研究棟
  • 年月日: 2009-06-19
• [学会発表] モデル検査に対応する上位ハードウェア記述言語MelasyのVHDLコード生成 (2009)
  • 著者名/発表者名: 野村達雄, 岩崎直木, 和崎克己
  • 学会等名: 情報処理学会第71回全国大会講演論文集,1,(2L-2),171-172
  • 発表場所: 立命館大学びわこ・くさつキャンパス
  • 年月日: 2009-03-11
• [学会発表] モデル検査に対応する上位ハードウェア記述言語MelasyとXML中間表現 (2009)
  • 著者名/発表者名: 岩崎直木, 野村達雄, 和崎克己
  • 学会等名: 情報処理学会第71回全国大会講演論文集,1,(2L-1),169-170
  • 発表場所: 立命館大学びわこ・くさつキヤンパス
  • 年月日: 2009-03-11
• [備考] ホームページ等
• [備考] 信州大学研究者総覧
  • URL: http://soar-rd.shinshu-u.ac.jp/profile/ja.gCnejaTN.html#books_articles_etc
• [備考] Mizar Proof Checking System
  • URL: http://markup.cs.shinshu-u.ac.jp/mirror/mizar/
• [備考] Formalized Mathematics(論文誌)
  • URL: http://versita.metapress.com/content/121073/