| 研究課題/領域番号 |
11680358
|
|---|
| 研究機関 | 大阪大学 |
|---|
研究代表者 |
谷口 健一 大阪大学, 大学院・基礎工学研究科, 教授 (00029513)
|
|---|
| 研究分担者 |
岡野 浩三 大阪大学, 大学院・基礎工学研究科, 講師 (70252632)
北道 淳司 大阪大学, 情報処理教育センター, 講師 (20234271)
東野 輝夫 大阪大学, 大学院・基礎工学研究科, 教授 (80173144)
山口 弘純 大阪大学, 大学院・基礎工学研究科, 助手 (80314409)
北嶋 暁 大阪大学, 大学院・基礎工学研究科, 助手 (00304030)
|
|---|
| キーワード | 拡張有限状態機械 / 時間オートマトン / 記号モデル検査 / プレスブルガー文 / out-of-order型パイプラインCPU |
|---|
| 研究概要 |
本年度は以下の研究を行なった。
1.並行動作順序回路としてきわめて有用な、あるクラスのout-of-order型パイプラインCPUに対する設計検証手法をいままでに提案してきたが、この手法を整理した。
2.時間制約付きで複数の並行動作回路を記述できるモデルとして、Alurの時間オートマトンを大域変数付きに拡張したモデルTASVを提案し、そのモデル上でのデッドロックフリー性を効率よく判定する判定手法を考案した。提案するアルゴリズムでは、大域変数の値が依存するような2つのオートマトン間に対して、大域的にはその変数制約を無視しても良いという十分条件を満たすのであれば、その2つのオートマトンのデッドロックフリー性を独立に判定するという効率上の工夫を行なっている。この手法を本年は、MMNS'99(ICPP'99 workshop)で発表した。
3.並行動作順序回路を記述できるモデルとして、整数レジスタを持つEFSMに着目し、単体のEFSMに対する時相論理式の記号モデル検査アルゴリズムを考案した。このアルゴリズムでは整数上の論理判定を用いて整数レジスタの桁数に依存せず判定を行なう工夫や、無限の状態集合を、条件選択の制約式のクラスの有用性を損なうことなく,、有限の領域として抽象化する工夫などを行なっているため、従来のBDD等を用いた手法では検査できなかった規模の回路の正しさを、実用時間で検証できるようになった。例題としてTCPD'94で提案されたベンチマーク問題の一部とビデオ電話の標準規格であるH.223を選び、実際に適用した。これらの結果をまとめた論文を研究集会で発表予定である。また、この結果は、並行動作順序回路にも比較的容易に適用可能であると考え、現在そのための具体的手法を考案中である。
|
