• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2012 年度 実施状況報告書

BDDとSATソルバを組み合わせた高多重度論理診断手法とECOコスト削減への応用

研究課題

研究課題/領域番号 24500064
研究種目

基盤研究(C)

研究機関神戸大学

研究代表者

沼 昌宏  神戸大学, 工学(系)研究科(研究院), 教授 (60188787)

研究分担者 黒木 修隆  神戸大学, 工学(系)研究科(研究院), 准教授 (90273763)
研究期間 (年度) 2012-04-01 – 2015-03-31
キーワードVLSI設計技術 / 論理診断 / SATソルバ
研究概要

(1) BDDとSATソルバを併用した論理診断手法の考案・実現
本研究の核心部分である論理診断処理に関して,BDDとSATソルバを併用した手法を考案・実現した。SATソルバは,大規模な論理回路に対する充足可能性判定を効率良く行える一方,BDDは限られた200変数程度までの論理回路に対して,乗算器等の例外を除いて多くの場合にその論理関数を効率良く表現して,論理関数同士の演算や,すべての充足解を陽に列挙することなくグラフ形式で陰に表現することが可能である点に特徴がある。具体的な処理手順について,まず形式的論理検証について,SATソルバを用いた充足可能性判定を行う。その結果,設計された論理回路に対して機能仕様との不一致が検出された場合は,論理診断処理を実行する。誤り追跡入力の生成など,多くの外部入力変数を扱う必要のある処理はSATソルバを用いるが,真理値シミュレーションのように,外部入力のほとんどが定数(0 or 1)で,修正箇所に対応する真理値変数のみを扱う場合には,真理値変数に関する制約条件をグラフ形式で陰に表現できるBDDを適用する点に特徴がある。BDDとSATソルバを併用することで,1万ゲート規模の論理回路に対しても効率よく論理診断処理が実現できることを確認した。
(2) 設計変更に対応した論理再合成部作成
(1) で考案・実現した手法に基づき,もとになる機能仕様が変更された際に,すでに合成された回路に対する可能な限り少ない修正によってその変更を満足させる,仕様変更に対応した論理再合成手法を考案し,ソフトウェアとして実現した。変更前の仕様に基づいて合成された回路が誤りを含むと考え,変更後の仕様を正しい機能とみなして論理診断・修正を行う。その結果,回路に対する最小の修正で,変更された仕様を満足することが可能となった。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

上記「研究業績の概要」に述べたように,交付申請書に記載した「研究の目的」について,ほぼ達成した。考案・実現した各手法の改良については今後の課題となっているが,この点についても,当初の計画通りである。

今後の研究の推進方策

昨年度の交付申請書に記載した通り,今後はBDDとSATソルバを併用した論理診断手法の改良,マスク再利用部の作成のほか,提案手法の評価と研究成果発表を中心に研究を進めていく。

次年度の研究費の使用計画

該当なし

  • 研究成果

    (2件)

すべて その他

すべて 学会発表 (2件)

  • [学会発表] メタル配線により再構成可能なセルと論理再合成への応用

    • 著者名/発表者名
      下野友大, 天満 健, 千崎弘人, 廣瀬哲也, 黒木修隆, 沼 昌宏
    • 学会等名
      DAシンポジウム2012
    • 発表場所
      ホテル下呂温泉水明館
  • [学会発表] 充足可能性判定に基づく誤り追跡入力生成と機能特定を用いた論理診断手法

    • 著者名/発表者名
      片山直樹, 松山友紀, 渡辺浩介, 廣瀬哲也, 黒木修隆, 沼 昌宏
    • 学会等名
      DAシンポジウム2012
    • 発表場所
      ホテル下呂温泉水明館

URL: 

公開日: 2014-07-24  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi