| 研究概要 |
(1)論理診断処理のSAT問題による定式化とSATソルバを用いた論理診断手法の考案・実現
本研究の核心部分である論理診断処理に関して,新たに充足可能性(SAT)問題による定式化を行った。従来はBDD(二分決定グラフ)によって表現された論理関数に基づいて行っていた修正解の適合性判定処理を,定式化された充足可能性問題を解くSATソルバを用いて実現可能となるように工夫した。より具体的には,SATソルバを適用するために,AND,OR等の論理関数演算に関して従来のBDDのように直接演算処理を呼び出す形ではなく,一旦その演算を含んだCNF式を生成してから,充足可能性判定によって論理診断処理が行えるような手法を考案した。
(2)設計変更に対応した論理再合成部作成
(1)で考案・実現した手法に基づき,もとになる機能仕様が変更された際に,すでに合成された回路に対する可能な限り少ない修正によってその変更を満足させる,仕様変更に対応した論理再合成手法を考案した。変更前の仕様に基づいて合成された回路が誤りを含むと考え,変更後の仕様を正しい機能とみなして論理診断・修正を行う。その結果,回路に対する最小の修正で,変更された仕様を満足することを可能とした。
|
