1999 Fiscal Year Annual Research Report
| Project/Area Number |
11680358
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
谷口 健一 大阪大学, 大学院・基礎工学研究科, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
岡野 浩三 大阪大学, 大学院・基礎工学研究科, 講師 (70252632)
北道 淳司 大阪大学, 情報処理教育センター, 講師 (20234271)
東野 輝夫 大阪大学, 大学院・基礎工学研究科, 教授 (80173144)
山口 弘純 大阪大学, 大学院・基礎工学研究科, 助手 (80314409)
北嶋 暁 大阪大学, 大学院・基礎工学研究科, 助手 (00304030)
|
|---|
| Keywords | 拡張有限状態機械 / 時間オートマトン / 記号モデル検査 / プレスブルガー文 / out-of-order型パイプラインCPU |
|---|
| Research Abstract |
本年度は以下の研究を行なった。
1.並行動作順序回路としてきわめて有用な、あるクラスのout-of-order型パイプラインCPUに対する設計検証手法をいままでに提案してきたが、この手法を整理した。
2.時間制約付きで複数の並行動作回路を記述できるモデルとして、Alurの時間オートマトンを大域変数付きに拡張したモデルTASVを提案し、そのモデル上でのデッドロックフリー性を効率よく判定する判定手法を考案した。提案するアルゴリズムでは、大域変数の値が依存するような2つのオートマトン間に対して、大域的にはその変数制約を無視しても良いという十分条件を満たすのであれば、その2つのオートマトンのデッドロックフリー性を独立に判定するという効率上の工夫を行なっている。この手法を本年は、MMNS'99(ICPP'99 workshop)で発表した。
3.並行動作順序回路を記述できるモデルとして、整数レジスタを持つEFSMに着目し、単体のEFSMに対する時相論理式の記号モデル検査アルゴリズムを考案した。このアルゴリズムでは整数上の論理判定を用いて整数レジスタの桁数に依存せず判定を行なう工夫や、無限の状態集合を、条件選択の制約式のクラスの有用性を損なうことなく,、有限の領域として抽象化する工夫などを行なっているため、従来のBDD等を用いた手法では検査できなかった規模の回路の正しさを、実用時間で検証できるようになった。例題としてTCPD'94で提案されたベンチマーク問題の一部とビデオ電話の標準規格であるH.223を選び、実際に適用した。これらの結果をまとめた論文を研究集会で発表予定である。また、この結果は、並行動作順序回路にも比較的容易に適用可能であると考え、現在そのための具体的手法を考案中である。
|
-
[Publications] 竹中 崇: "整数入力値を保持するレジスタを持つ EFSM に対する記号モデル検査アルゴリズム"電子情報通信学会第13回回路とシステム(軽井沢)ワークショップ. (発表予定) (1999)
-
[Publications] Kozo Okano: "Specification of Real-time Systems using a Timed Automata Model with Shared Variables and Verification of Partial-deadlock Freeness"Proceedings of the 1999 ICPP Workshops. 576-581 (1999)
-
[Publications] 竹中 崇: "あるクラスの Out-of-order 型パイプライン CPU の設計の正しさの十分条件とその形式的検証"情報処理学会論文誌. Vol.40,No.4. 1587-1596 (1999)
