ハードウェアの高位設計・検証支援システム

2003 Fiscal Year Annual Research Report

• Project/Area Number: 13558028
• Research Institution: Osaka University
• Principal Investigator: 谷口 健一 大阪大学, 大学院・情報科学研究科, 教授 (00029513)
• Co-Investigator(Kenkyū-buntansha): 岡野 浩三 大阪大学, 大学院・情報科学研究科, 助教授 (70252632) ; 北道 淳司 会津大学, コンピュータ理工学部, 助教授 (20234271) ; 東野 輝夫 大阪大学, 大学院・情報科学研究科, 教授 (80173144) ; 森岡 澄夫 ソニー(株), ユビキタス技術研究所, 研究員 ; 山口 弘純 大阪大学, 大学院・情報科学研究科, 助手 (80314409)
• Keywords: 整数変数つきFSM / プレスブルガー文 / 時相論理式 / 自動検証 / 時間オートマトン群 / 実時間システム

Research Abstract

本研究では,ハードウェア設計においてVHDL風の記述からレジスタ転送レベルの正しい設計を得る方法論の確立を目指している.本研究の一つの課題としてレジスタ転送レベルの設計における(いつかは条件を満たす,いつも条件を満たしているなどの)時相性質の検証方法があげられる.そこで,レジスタ転送レベルを表現するのに適したモデルである整数変数を持つFSM(有限状態機械)を対象に,時相性質を自動検証する方法を考案した.そして,その結果を電子情報通信学会論文誌にて発表した.提案手法では外部入力を許すモデルに対し,いくつかのクラス制約のもとで自動検証を可能にしている.検証にはプレスブルガー文の真偽判定ルーチンの一つであるオメガ処理系を用いている.現在研究室ではオメガと同等以上の表現式が扱え,かつ,実行時間についても遜色のない判定ルーチンを関数型プログラミング言語MLで開発し,有効であることを確認している.ハードウェアの設計検証の主たる判定ルーチンとしてそれを用いる予定である.ハードウェアの設計においてはスループット,遅延の要求に対する保証も考慮に入れる必要がある.これらの要求性質に対し,時間オートマトンを用いた検証方法の理論的妥当性を示し,国際会議ICFEM2003(LNCS2885)で発表した.
今後は次の展開を考えている.VHDL風の記述と時間指定から時間オートマトンに変換する,あるいは逆変換する処理系の作成,及び,プレスブルガー文真偽判定の処理系の開発支援システムヘの統合を行いたい.また,上述ICFMで提案した時間オートマトンベースによる時間制約検証法,及び,それを満たす実装に関する方法論をハードウェアに適用し,そのような時間要求を満たす設計法を確立したい.最終的に、これらの方法論の有用性を例題により調べたいと考えている.

Research Products

• [Publications] 竹中 崇: "外部入力値のみを保持できる整数変数を持つFSMに対する記号モデル検査法"電子情報通信学会論文誌 D-I. Vol.J-87 D1,No.4(To appear). (2004)
• [Publications] Behzad Bordbar: "Verification of Timeliness QoS Properties in Multimedia Systems"Lecture Notes in Computer Science. 2885. 524-540 (2003)