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

大規模論理設計の形式的検証に関する研究

Research Project

Project/Area Number 08680380
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionKyoto Sangyo University

Principal Investigator

平石 裕実  京都産業大学, 工学部, 教授 (40093299)

Project Period (FY) 1996
Project Status Completed (Fiscal Year 1996)
Budget Amount *help
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 1996: ¥2,200,000 (Direct Cost: ¥2,200,000)
Keywords形式的検証 / 設計検証 / 論理設計 / 時相論理 / 記号モデル検査 / 耐故障設計 / セルフテスト / セルフチェック
Research Abstract

本年度は、主として時空間様相論理の並列検証アルゴリズムの基礎的研究と、具体的な設計検証問題として耐故障設計の形式的検証を行なった。
1.時空間様相論理の並列検証アルゴリズム:時空間様相論理の検証アルゴリズムでは、時間方向と空間方向の逆像計算が中心になる。これらの逆像計算の並列アルゴリズムとして、CPUの個数が数個から十数個程度の高性能ワークステーション上での実行に適したアルゴリズムと、50台程度のワークステーションを高速ネットワークで結合した分散システム上での実行に適したアルゴリズムの基礎的研究を行なった。前者では、マルチスレッドに基づく並列アルゴリズムを種々検討し、後者では、各ワークステーションで共有すべきデータの管理手法を種々検討した。その結果、並列処理の正当性を確保するために、種々の共有データへのアクセスの際にロックをかける必要があるが、ロックの方法やキャッシュの方法が効率に大きな影響を及ぼすことが判明した。今後引続き研究を進める必要があると考えられる。
2.耐故障設計の形式的検証:論理回路の耐故障設計では、設計した回路がセルフテスト性やセルフチェック性を持つことが要求される場合が多い。これらの性質は回路内部に故障を仮定した上で満たされるべき性質であり、その検証は煩雑になる。そこで、これらの性質を論理関数で表現し、論理関数処理でこれらの性質の検証を行うアルゴリズムを示し、実際に論理シミュレーションによる検証に比べて数倍高速に検証できることを示した。

Report

(1 results)
  • 1996 Annual Research Report
  • Research Products

    (2 results)

All Other

All Publications (2 results)

  • [Publications] K.Kawakubo: "Formal Verification of Self-Testing Properties of Combinational Circuits" Proc.5th Asian Test Symposium. 119-122 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] K.Kawakubo: "Formal Verification of Totally Self-Checking Properties of Combinational Circuits" IEICE Trans.Information and Systems. E80-D(1). 57-62 (1997)

    • Related Report
      1996 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi