| 研究分担者 |
東野 輝夫 大阪大学, 大学院・情報科学研究科, 教授 (80173144)
北道 淳司 会津大学, コンピュータ理工学部, 助教授 (20234271)
岡野 浩三 大阪大学, 大学院・情報科学研究科, 助教授 (70252632)
山口 弘純 大阪大学, 大学院・情報科学研究科, 助手 (80314409)
森岡 澄夫 ソニー(株), ユビキタス技術研究所, 研究員
|
|---|
| 研究概要 |
本研究は,定用途向けICの設計において,実現アーキテクチャに依存しない抽象レベルの動作仕様に対するレジスタ転送レベル(RTL)記述の設計の正しさを論理的に保証するための方法論の確立や支援系作成,および,手法とシステムの有用性を評価することをその目的としている.
研究グループでは平成6年度科学研究補助金「ASIC設計の上流工程設計支援システムの開発」,平成9年度科学研究補助金「通信プロトコルの形式仕様からのハードウェア回路合成」などでRTレベルの検証支援系や,高位記述からRTレベルの記述変換系を試作し,有用性を評価してきた.この検証支援系を元に,本研究ではより上位の記述における,時間制約遵守性の保証とコンポーネントベースの機能検証に焦点を絞り研究を行ってきた.
検証対象は大きく,時間制約の遵守性の保証とハードウェアコンポーネントの機能性質の保証の2面に分けることができる.時間制約の遵守性については近年研究が盛んな時間オートマトンやそれらに対する検証支援システムを有効に利用する方法を考案した.また,機能検証においては,コンポーネントベース指向設計の方針をとり,従来の形式的検証手法と併せた検証手法を考案し,支援システムを作成した.本研究では上位仕様記述としてステートチャートの時間拡張モデルに着目し,時間制約遵守性と機能検証の検証手法について具体的に以下の研究を行った.
1.時間制約の遵守性について:
(エ)整数変数をもつあるクラスの有限機械モデルに対する記号検査アルゴリズムの提案
(オ)時間オートマトンを用いた時間制約遵守性検証手法の提案
(カ)及び,時間領域デッドロック判定法の提案
2.ハードウェアコンポーネントの機能性質の検証について:
(エ)コンポーネントベースの関数型言語向けの検証支援システムの試作
|
