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

2009 Fiscal Year Annual Research Report

高位ハードウェア設計記述に対するモデル検査手法の研究

Research Project

Project/Area Number 19500043
Research InstitutionOsaka University

Principal Investigator

浜口 清治  Osaka University, 大学院・情報科学研究科, 准教授 (80238055)

Keywords設計検証 / フォーマル検証 / 第一階述語論理 / モデル検査 / 高位ハードウェア検証
Research Abstract

近年のハードウェア設計では,設計検証が設計工程の半分以上を占めるようになっている.近年,設計および検証効率を改善するため,ハードウェア設計を高位の言語で記述するアプローチが実用的にも取り入れられるようになってきているが,とくに,高位のハードウェア記述に対するフォーマル検証手法については,必ずしも十分な研究が行われているとは言えない.本研究では,C言語などで記述された高位ハードウェアの設計に対するフォーマル検証手法,とくにモデル検査の手法を開発することを目的とする.平成21年度は特に次の点について研究を行って成果を得た.
・複数の論理体系を組み合わせた近似的モデル検査アルゴリズムの実装と評価
前年度までに得られていた複数の論理体系を組み合わせた有界モデル検査の手法と,EUF(限量子を含まない等号付き第一階述語論理)に対する近似的な非有界モデル検査の手法を融合して,さらに,利用する複数の論理体系を動的に変化させる手法を新たに導入することにより,非有界モデル検査が可能なアルゴリズムを考案・実装し,評価を行った.この手法では,当初はEUFのみで検証を行って,うまく行かなかった場合に,線形算術論理,ビットベクトル論理と順番に論理体系を切り替えて,検証の近似度をさげていく.これにより,前年度までに開発手法を含む従来手法では扱うことができなかった,信号処理プログラム(ADPCM)の例題について,現実的な時間(~250秒程度)で検証可能となることを示した.

  • Research Products

    (3 results)

All 2010 2009

All Journal Article (1 results) (of which Peer Reviewed: 1 results) Presentation (2 results)

  • [Journal Article] Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic2010

    • Author(s)
      Hiroaki Shimizu
    • Journal Title

      IPSJ Transactions on System LSI Design Methodology 4

      Pages: 105-117

    • Peer Reviewed
  • [Presentation] 第一階述語論理のサブクラスに対する近似的モデル検査アルゴリズム2009

    • Author(s)
      増田和也
    • Organizer
      第142回システムLSI設計技術研究会
    • Place of Presentation
      高知市文化プラザ (高知)
    • Year and Date
      2009-12-02
  • [Presentation] SMTソルバーを利用した近似的な非有界モデル検査アルゴリズムにおける複数の論理体系の組み合わせ手法2009

    • Author(s)
      浜口清治
    • Organizer
      組み込みシステムシンポジウム2009
    • Place of Presentation
      国立オリンピック記念青少年総合センター (東京)
    • Year and Date
      2009-10-22

URL: 

Published: 2011-06-16   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi