2009 Fiscal Year Annual Research Report
SATソルバを利用した論理診断手法とLSI設計変更コスト削減への応用
| Project/Area Number |
21500054
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
沼 昌宏 Kobe University, 工学研究科, 教授 (60188787)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
黒木 修隆 神戸大学, 工学研究科, 准教授 (90273763)
|
|---|
| Keywords | 論理診断 / 論理再合成 / 設計変更 / SAT / 設計誤り / 診断対象回路 |
|---|
| Research Abstract |
(1)論理診断処理のSAT問題による定式化とSATソルバを用いた論理診断手法の考案・実現
本研究の核心部分である論理診断処理に関して,新たに充足可能性(SAT)問題による定式化を行った。従来はBDD(二分決定グラフ)によって表現された論理関数に基づいて行っていた修正解の適合性判定処理を,定式化された充足可能性問題を解くSATソルバを用いて実現可能となるように工夫した。より具体的には,SATソルバを適用するために,AND,OR等の論理関数演算に関して従来のBDDのように直接演算処理を呼び出す形ではなく,一旦その演算を含んだCNF式を生成してから,充足可能性判定によって論理診断処理が行えるような手法を考案した。
(2)設計変更に対応した論理再合成部作成
(1)で考案・実現した手法に基づき,もとになる機能仕様が変更された際に,すでに合成された回路に対する可能な限り少ない修正によってその変更を満足させる,仕様変更に対応した論理再合成手法を考案した。変更前の仕様に基づいて合成された回路が誤りを含むと考え,変更後の仕様を正しい機能とみなして論理診断・修正を行う。その結果,回路に対する最小の修正で,変更された仕様を満足することを可能とした。
|
