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

マイクロプロセッサの形式的仕様記述・検証に関する研究

Research Project

Project/Area Number 06780256
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field 計算機科学
Research InstitutionKyoto University

Principal Investigator

濱口 清治  京都大学, 工学部, 講師 (80238055)

Project Period (FY) 1994
Project Status Completed (Fiscal Year 1994)
Budget Amount *help
¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1994: ¥900,000 (Direct Cost: ¥900,000)
Keywords時相論理 / 論理設計 / マイクロプロセッサ / 形式的検証 / モデルチェッキング / 仕様記述 / 二分決定グラフ
Research Abstract

交付申請書に記載の通り、次の通り研究を行った。
(1)形式的設計検証に関する研究
従来の等価性や包含性の概念のもとでは、パイプライン処理などを行うマイクロプロセッサの等価性を論じることは難しかった。そこで、本研究では、レジスタやメモリなど命令セットによって仮定されている資源それぞれにおける値の変化に注目して、パイプラインやス-パスケーラなど種々の設計に対して、統一的な等価性の定義を与え、また、これに基づいた検証手法を開発した。また、この手法を実装するためには、大規模な回路の表現する関数に対する等価性判定など種々の演算を高速にまた少ない記憶容量で実現する必要性があることが明らかとなったため、二分モーメントグラフと呼ばれる、関数の新しい表現手法を導入して、特に従来手法では指数時間を要した乗算器に対する多項式時間の処理方式を新たに示した。これらの手法を融合させたマイクロプロセッサの検証システムの開発が今後の課題である。
(2)仕様記述に関する研究
これまで時相論理による仕様記述に対する検証手法の開発を行ってきており、この際、主に検証効率が良いことから分岐時間型の時相論理を用いてきたが、記述が直観に反し、繁雑であるといった問題点があった。これに対して、本研究では線形時間型の時相論理に基づく論理関数処理を用いた手法を開発・実装した。

Report

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

    (2 results)

All Other

All Publications (2 results)

  • [Publications] Edmund M.Clarke: "Another Look at LTL Model Checking" Proc.of Cenf.on Computer-Aided Verification Lecture Notos. 818. 415-427 (1994)

    • Related Report
      1994 Annual Research Report
  • [Publications] 平石裕実: "論理関数処理に基づく形式的検証手法" 情報処理学会誌. 35. 710-718 (1994)

    • Related Report
      1994 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi