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

順序回路のタイミング解析の正確さ向上に関する研究

Research Project

Project/Area Number 18700043
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Computer system/Network
Research InstitutionNagoya University

Principal Investigator

中村 一博  Nagoya University, 情報科学研究科, 助教 (90335076)

Project Period (FY) 2006 – 2007
Project Status Completed (Fiscal Year 2007)
Budget Amount *help
¥2,800,000 (Direct Cost: ¥2,800,000)
Fiscal Year 2007: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2006: ¥2,300,000 (Direct Cost: ¥2,300,000)
KeywordsVLSI設計技術 / 順序回路 / SATソルバ / CNF式 / タイミング解析 / 論理回路 / VLSI / 形式的検証 / BDD
Research Abstract

論理式の充足可能性判定(Satisfiability;SAT)ベースの形式的検証やタイミング解析の高速化のための、和積標準形(Conjunctive Normal Form;CNF)論理式生成における回路分割手法の開発を行った。論理回路のCNF式表現は一意でない上、SATソルバでの処理時間は、与えられるCNF式により変化するため、論理回路をCNF式に変換する処理は、SATべースの形式的検証やタイミング解析の高速化を図る上で重要である。この変換処理において、論理回路をファンアウトポイントで分割し、部分回路毎にCNF式に変換するアルゴリズムの開発を行った。提案アルゴリズムを実装し、SATソルバの実行時間について評価を行ったところ、従来の変換手と比較して、SATソルバの実行時間の短縮が確認できた。本研究の成果は国内研究会で発表した。
また、順序回路の形式的検証やタイミング解析の高速化のための、1-hotカウンタ検出手法の開発を行った。形式的検証やタイミング解析の正確さを向上させる上で、初期状態から到達可能な状態の正確な解析は重要である。1-hotカウンタは、高速な順序回路の設計においてよく用いられるが、とりうる値が限られているため、多くの状態が到達不能である。1-hotカウンタを検出し、到達可能な状態をより正確に解析することが、1-hotカウンタを含む順序回路の形式的検証やタイミング解析の正確さ向上につながる。1-hotカウンタ検出問題の定式化を行うとともに、1-hotカウンタ検出アルゴリズムの開発を行った。本研究の成果は国内研究会で発表した。

Report

(2 results)
  • 2007 Annual Research Report
  • 2006 Annual Research Report
  • Research Products

    (3 results)

All 2007

All Journal Article (3 results)

  • [Journal Article] SATベース形成的検証の高速化のためのCNF式生成における回路分割手法2007

    • Author(s)
      成瀬智啓、中村一博、高木一義、高木直史
    • Journal Title

      DAシンポジウム2007論文集

      Pages: 5560-5560

    • Related Report
      2007 Annual Research Report
  • [Journal Article] 順序回路の形成的検証のための1-hotカウンタ検出手法2007

    • Author(s)
      中村一博、高木一義、高木直史
    • Journal Title

      電子情報通信学会基礎・境界ソサイエティ大会論文集 A-3-8

      Pages: 52-52

    • Related Report
      2007 Annual Research Report
  • [Journal Article] 論理回路のSATべース形式的検証の高速化のためのBDDを用いたCNF式生成手法2007

    • Author(s)
      中村一博
    • Journal Title

      電子情報通信学会技術報告 CPSY2006-95

      Pages: 61-66

    • Related Report
      2006 Annual Research Report

URL: 

Published: 2006-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi