| 研究分担者 |
杉山 裕二 岡山大学, 工学部, 教授 (50116050)
岡野 浩三 大阪大学, 基礎工学部, 助手 (70252632)
北道 淳司 大阪大学, 基礎工学部, 助手 (20234271)
松浦 敏雄 大阪大学, 情報処理教育センター, 助教授 (40127296)
東野 輝夫 大阪大学, 基礎工学部, 助教授 (80173144)
|
|---|
| 研究概要 |
1.ハードウェアの上流工程設計に特有な証明技法や設計支援のための基本機能を検討し,設計支援システムの全体設計を行った.本年度は,記述支援系,検証支援系,自動化ルーチンを作成した.
2.記述支援系は,従来我々の研究グループで開発してきたASL記述支援系をもとに作成した.
3.検証は,上位レベルの状態遷移を実現する下位レベルの状態遷移の系列に繰返しがある場合,途中状態において各部品間に成り立つべき不変表明を用いた構造的帰納法で行われるが,証明失敗による不変表明の修正などの試行錯誤が多く,設計検証を容易に,かつなるべく自動的に行う必要がある.そこで,以下の機能を有する検証支援系を作成した.(1)上位レベルの状態遷移と対応する下位レベルの状態遷移の系列を状態遷移図として表示する機能.(2)不変表明の変更により,再度検証すべき箇所を表示する機能.(3)整数上の論理式の高速な恒真性判定ルーチン.また,使用する部品,設計したバスアーキテクチャ及び入力論理やマイクロプログラムによって上位レベルの各データ転送や実行制御を実現しているかどうかを自動的に証明するルーチンも作成した.
作成した検証支援系を用いて,マックスソート回路やCPU等の例題回路の設計検証を行い,試行錯誤は伴うが,検証者が容易にかつ高速に検証を行うことができた.長さ1000程度の大きな論理式でも数秒程度で恒真性の判定が行えた.
4.設計自動化ルーチンの一部として,冗長な状態遷移を除去して実行効率を向上させるための10数個の状態図変形ルーチンを作成した.マックスソートなど例題設計において適用を行った結果,さらに2,3のルールを実現する必要があり,今後,効果的なルールの適用法等について検討していく必要がある.
5.本年度作成した支援系を用いていくつかの設計及びその検証を行い,その結果についていくつか研究報告を行った.
|
