2004 Fiscal Year Annual Research Report
| Project/Area Number |
13558028
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
谷口 健一 大阪大学, 大学院・情報科学研究科, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
東野 輝夫 大阪大学, 大学院・情報科学研究科, 教授 (80173144)
北道 淳司 会津大学, コンピュータ理工学部, 助教授 (20234271)
岡野 浩三 大阪大学, 大学院・情報科学研究科, 助教授 (70252632)
山口 弘純 大阪大学, 大学院・情報科学研究科, 助手 (80314409)
森岡 澄夫 ソニー(株), ユビキタス技術研究所, 研究員
|
|---|
| Keywords | ハードウェア高位設計 / 機能性質の保証 / 時間性質の保証 / 検証支援システム / レジスタ転送レベル / 動作仕様レベル / 時間領域デッドロック |
|---|
| Research Abstract |
本研究は,ハードウェアの高位設計と検証を行うための方法論の確立と支援ツール作成を目指している.検証対象は大きく,時間制約の遵守性の保証とハードウェアコンポーネントの機能性質の保証の2面に分けることができる.研究グループの別プロジェクトにより,ステートチャートと時間指定から,時間オートマトン群へ変換する変換系を作成しており,これを用いて,スループットや遅延などの時間性質の自動検証を行う方法を確立している.ハードウェアの制御部は,時間制約を持ち制御変数にレジスタの有限値しか使わないステートチャートを用いて記述することにより,時間性質の検証を実用時間で行える.また,この時間制約を持つステートマシンによりハードウェアの上位レベルの振る舞いとしての機能仕様も記述できるため,研究グループの従来研究の成果と併せて,ハードウェアの機能性質の検証も可能である.また,研究グループでは,関数型言語向けの検証支援システムを作成している.ハードウェアの要求記述は関数型言語を用いて記述可能であり,このシステム上でハードウェアコンポーネント単位でのより柔軟な検証作業を行える.今年度は,限定されたクラスの言語の相互変換ツールを作成した.このツールにより,動作仕様レベルの記述をステートチャート記述からJava,VHDL等の記述として得ることができる.以上により,ハードウェアの高位設計の設計の正しさについて時間性質と機能性質の両方から保証する手法を確立できた.
また,時間領域デッドロック(可能な動作がいずれも起こらないと時間の経過に伴って動作不能になる状況)の検出について,この問題を有理数プレスブルガー文真偽判定問題に帰着し判定する方法を考案し,国際会議で発表した.この手法は時間オートマトンを対象にしており,上記のステートチャート時間オートマトン変換システムと併せて,上位レベルの検証が可能となる.
|
