2012 Fiscal Year Research-status Report
ＢＤＤとＳＡＴソルバを組み合わせた高多重度論理診断手法とＥＣＯコスト削減への応用
| Project/Area Number |
24500064
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Kobe University |
|---|
Principal Investigator |
沼 昌宏 神戸大学, 工学(系)研究科(研究院), 教授 (60188787)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
黒木 修隆 神戸大学, 工学(系)研究科(研究院), 准教授 (90273763)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | ＶＬＳＩ設計技術 / 論理診断 / SATソルバ |
|---|
| Research Abstract |
(1) BDDとSATソルバを併用した論理診断手法の考案・実現
本研究の核心部分である論理診断処理に関して，BDDとSATソルバを併用した手法を考案・実現した。SATソルバは，大規模な論理回路に対する充足可能性判定を効率良く行える一方，BDDは限られた200変数程度までの論理回路に対して，乗算器等の例外を除いて多くの場合にその論理関数を効率良く表現して，論理関数同士の演算や，すべての充足解を陽に列挙することなくグラフ形式で陰に表現することが可能である点に特徴がある。具体的な処理手順について，まず形式的論理検証について，SATソルバを用いた充足可能性判定を行う。その結果，設計された論理回路に対して機能仕様との不一致が検出された場合は，論理診断処理を実行する。誤り追跡入力の生成など，多くの外部入力変数を扱う必要のある処理はSATソルバを用いるが，真理値シミュレーションのように，外部入力のほとんどが定数（0 or 1）で，修正箇所に対応する真理値変数のみを扱う場合には，真理値変数に関する制約条件をグラフ形式で陰に表現できるBDDを適用する点に特徴がある。BDDとSATソルバを併用することで，1万ゲート規模の論理回路に対しても効率よく論理診断処理が実現できることを確認した。
(2) 設計変更に対応した論理再合成部作成
(1) で考案・実現した手法に基づき，もとになる機能仕様が変更された際に，すでに合成された回路に対する可能な限り少ない修正によってその変更を満足させる，仕様変更に対応した論理再合成手法を考案し，ソフトウェアとして実現した。変更前の仕様に基づいて合成された回路が誤りを含むと考え，変更後の仕様を正しい機能とみなして論理診断・修正を行う。その結果，回路に対する最小の修正で，変更された仕様を満足することが可能となった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
上記「研究業績の概要」に述べたように，交付申請書に記載した「研究の目的」について，ほぼ達成した。考案・実現した各手法の改良については今後の課題となっているが，この点についても，当初の計画通りである。
|
| Strategy for Future Research Activity |
昨年度の交付申請書に記載した通り，今後はBDDとSATソルバを併用した論理診断手法の改良，マスク再利用部の作成のほか，提案手法の評価と研究成果発表を中心に研究を進めていく。
|
| Expenditure Plans for the Next FY Research Funding |
該当なし
|
