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

2006 年度 研究成果報告書概要

高位ハードウェア設計記述に対する等価性判定手法の研究

研究課題

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

基盤研究(C)

配分区分補助金
応募区分一般
研究分野 計算機システム・ネットワーク
研究機関大阪大学

研究代表者

浜口 清治  大阪大学, 大学院情報科学研究科, 助教授 (80238055)

研究期間 (年度) 2004 – 2006
キーワードフォーマル検証 / 第一階述語論理 / 高位ハードウェア検証 / 充足可能性判定
研究概要

近年のハードウェア設計では,設計検証に要する時間が増加しつづけ,全設計工程の60%--80%もの時間を占めるようになっている.これに対して,フォーマル検証の適用が始まっているが、これらの多くはレジスタ転送レベルやゲートレベルより高位の設計には適用できない.本研究では、C言語などで書かれた高位のハードウェア記述に対して,2つの記述の機能の等価性判定を行う手法を研究する.具体的には,記述中にあらわれる算術演算を,第1階述語論理における関数記号によって表現し,意味を解釈せずに記号のまま処理することにより,効率化を図る.
この手法の問題は,2つの記述が極めて似通っていなければ等価と判定することができないという点である.これを補うため,本研究では,同値制約のもとでの等価性判定アルゴリズムの検討と実装を行った.この同値制約は,(x>1⇔x-1>0)といった形の規則であり,等価とみなすべきパターンを与えるために用いる.ブール式の充足可能性判定で用いられているコンフリクト解析と呼ばれる手法を拡張して実装することにより,PARCORフィルタ,ADPCMフィルタ,フーリエ変換処理,平方根計算のプログラムに対する等価性判定に適用を試みた.その結果,乗算等より複雑な演算(非線形の演算)を含む場合には,従来のプール関数レベルでの等価性判定手法に比べ,1-2桁程度高速,あるいは従来の手法では計算量的に判定困難であるような規模でも判定が可能となることが明らかとなった.

  • 研究成果

    (2件)

すべて 2006 2004

すべて 雑誌論文 (2件)

  • [雑誌論文] Satisfiability Checking under Equivalence Constraints for a Decidable Subclass of First-Order Logic2006

    • 著者名/発表者名
      Hiroaki Kozawa
    • 雑誌名

      Proceedings of the 13th Workshop on Synthesis And System Integration of Mixed Information technologies 13

      ページ: 363-368

    • 説明
      「研究成果報告書概要(和文)」より
  • [雑誌論文] Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas2004

    • 著者名/発表者名
      Atsushi Moritomo
    • 雑誌名

      2nd International Conference on Automated Technology for Verification and Analysis, Lecture Notes 3299

      ページ: 108-119

    • 説明
      「研究成果報告書概要(和文)」より

URL: 

公開日: 2008-05-27  

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

Powered by NII kakenhi