权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

動作レベルおよびレジスタ転送レベルのハードウェア記述に対する形式的検証手法の研究

行为层和寄存器传输层硬件描述形式化验证方法研究

基本信息

批准号：
13780233
负责人：
濱口清治
金额：
$ 1.22万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2001
资助国家：
日本
起止时间：
2001 至 2002
项目状态：
已结题

项目摘要

本研究課題では,動作レベルの記述を扱うことができるフォーマル検証技術の確立を目指している.この背景には,今後,設計生産性向上のため,動作レベルからの設計および自動合成が広く利用されるようになるであろうという予測がある.具体的な研究テーマとして,記号シミュレーションを利用した,動作レベル/レジスタ転送レベルの検証手法に関して,次の点を目標とした.特にCプログラムで数百行相当,レジスタ転送レベルでの実行ステップ数が数万サイクルの設計を目標とした.1.記号シミュレーションに基づく等価性判定アルゴリズムの省メモリ化/高速化.2.プロパティ・チェック手法の開発.3.第1階述語論理の部分クラスに対する恒真性判定アルゴリズムの高速化.平成13年度は,3.のアルゴリズムの作成およびそれに基づく1.のアルゴリズムを実装して評価を行った.3.のアルゴリズムに対して「記号関数表」,1.のアルゴリズムに対して「強制同期」と名付けたヒューリスティクを用いることにより,研究開始前に作成していたプロトタイプに比べ,高速化と省メモリ化に成功した.具体的には,1GBのメモリを要し,24分かかった例題(DSPの設計例)を,386MBのメモリで4分で検証することができるようになった他,制御構造に2重ループを含むような例題(レジスタ転送レベルの実行サイクル数が37500サイクル)についても,検証が可能となった(検証時間は8時間20分).プロトタイプのシミュレータでは,必要記憶容量が大きすぎ,この例題を扱うことはできなかった.2.のプロパティチェックアルゴリズムについては,上記の記号シミュレータをベースにして,ユーザが与えた有限サイクル数分について,プロパティチェックを行うアルゴリズムを開発した.また,これを実装して,簡単な例題への適用を試みた.当初の計画通り,第一階述語論理の部分クラスに対する記号シミュレーションを,より大きな設計例へ適用できるようになりつつある.しかしながら,この部分クラスの論理のセマンティクスでは,本来等価となるべき例でも等価にならない場合がある.現在,この問題に対する解決策の1つとして,限定的な等式制約のもとでの等価性判定について検討を進めている.

The purpose of this study is to make a record of how to make sure that the technology is correct. In the future, the designer will make an up-of-the-box performance, and the auto-synthesis system will be used to monitor the performance of the device. For a specific study, please note that you can make use of it, do something about it, send it to you and click on it for the second time. There are hundreds of lines that are equivalent to each other, and the number of customers is tens of thousands of dollars. 1. The record number indicates that there is a difference in the performance of sexual judgment, such as basic information, etc. 2. Please do not know how to do it. 3. The first part of the article describes how to increase the speed of fidelity determination. The year of Pingcheng 13, 3. I don't know. I don't know. I don't know. I don't know what to do. 3. Please tell me about the number of ticks in the table, 1. During the same period of time, the system is required to be used in the same period. Before the start of the study, a trial was made before the start of the study, and the high-speed reduction was successful. For a specific example, 1GB airwaves, 24 minutes (DSP setting), and 386MB cycles, 4 minutes, four minutes, six minutes, six minutes, one hour, two minutes, one hour, one, two, two, one, two, one, two, two, one, two Since it is necessary to record a large amount of information, it is necessary to record a large capacity. This is a good example. Please do not know if you do not have any information, please, please, please. Please make sure that you install the device, and use the test device for the sample project. At the beginning of the plan, the first part of the plan was written in the first part of the plan, and the first part of the plan was written in the first part of the plan. I don't know what to do, I don't know, I don't know. At present, the solution of the problem is to solve the problem, and the limited equation is used to determine the performance of the problem.