ASIC設計の上流工程設計支援システムの開発

1993 Fiscal Year Annual Research Report

• Project/Area Number: 05558031
• Research Institution: Osaka University
• Principal Investigator: 谷口 健一 大阪大学, 基礎工学部, 教授 (00029513)
• Co-Investigator(Kenkyū-buntansha): 杉山 裕二 岡山大学, 工学部, 教授 (50116050) ; 岡野 浩三 大阪大学, 基礎工学部, 助手 (70252632) ; 北道 淳司 大阪大学, 基礎工学部, 助手 (20234271) ; 松浦 敏雄 大阪大学, 情報処理教育センター, 助教授 (40127296) ; 東野 輝夫 大阪大学, 基礎工学部, 助教授 (80173144)
• Keywords: 同期式順序回路 / 代数的手法 / 高位合成 / 段階的詳細化 / 形式的手法 / 設計自動化 / 設計検証 / 機能設計

Research Abstract

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

Research Products

• [Publications] 北道 淳司: "代数的手法を用いた同期式順序回路の方式・機能設計と検証例" 1993年秋期電子情報通信学会全国大会. Vol.1. 276-277 (1993)
• [Publications] 谷口健一: "代数的手法を用いた仕様記述と設計及び検証" 回路とシステム軽井沢ワークショップ論文集. 375-380 (1993)
• [Publications] 北道淳司: "代数的手法を用いた同期式順序回路の段階的設計法" 電子情報通信学会論文誌(A分冊). No.3(採録決定). (1993)
• [Publications] 森岡澄夫: "同期式順序回路の設計検証例" 情報処理DAシンポジウム'93論文集. 73-76 (1993)