1994 Fiscal Year Annual Research Report
| Project/Area Number |
06680310
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
米田 友洋 東京工業大学, 大学院情報理工学研究科, 助教授 (30182851)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
南谷 崇 東京工業大学, 大学院情報理工学研究科, 教授 (80143684)
|
|---|
| Keywords | 形式的検証 / 非同期式回路 / ペトリネット / 時相論理 / トレース理論 |
|---|
| Research Abstract |
本研究では,非同期式回路の設計段階において,設計した回路が所望の入出力関係を実現しているかどうかを,手軽にまたインタラクティブに確かめることができる設計検証システムを開発することを目的とする.本研究の成果は以下の4点である.(1)非同期式回路を記述するハードウェア記述言語としてVerilog風の記述言語から(タイム)ペトリネットへの変換ツールを開発し,若干のモジュール・ゲートレベルの各種ライブラリを作成した.また,出力支援環境として,フォーマット文を入力ファイルに書くことにより,ユーザが必要な信号線の変化の様子のみを出力できるにようにした.(2)回路をペトリネットで表し検証すべき性質をペトリネットで表す検証器,回路をタイムペトリネットで表し検証すべき性質を実時間線形時相論理で表す検証器,および回路をタイムペトリネットで表し検証すべき性質をタイムペトリネットで表す検証器の3つの検証器を統合し,同一の回路記述を用いて,いろいろな方法で記述された性質を検証できるようにした.(3)最初の検証器については,階層的検証方式をとっているが,さらに,net unfoldingという一種の半順序関係に基づく方式を組み合わせることを試みた.完全に実装は終わっていないが,可能であることを確認し,方法論をある程度確立した.(4)約20の回路について検証を行い,検証効率,使い良さ等について検討した.以上より,本研究の目的はほぼ達成できたが,さらに出力支援環境の充実および半順序関係に基づく方式の実装・評価が今後の課題である.
|
