論理関数の充足不可能性に注目した論理回路デバッグ手法の検討(設計技術,組込み技術とネットワークに関するワークショップETNET2012)
スポンサーリンク
概要
- 論文の詳細を見る
回路中の誤り箇所を特定するデバッグは時間のかかる作業である。従来手法では反例に基づいてデバッグを始めるが、本稿では反例が得られない状況におけるデバッグ方法を考える。論理関数の充足可能性(SAT)問題を用いた検証では、充足可能な場合に設計が正しくなるように定式化される場合、反例を特定することができない。この場合には、論理式中で矛盾を起こしている部分集合(UNSATコア)がデバッグのヒントになると考えられる。そこで本稿では、複数のUNSATコアを用いることで、誤り候補を絞り込む手法を考える。しかし、UNSATコアを多数求めようとすると、現在のアルゴリズムでは計算量が爆発的に増加し、このままでは使えないという問題がある。本稿では、簡単な回路を対象に上記の方法を説明し、問題点を克服するための考察を行う。
- 2012-02-24
著者
-
藤田 昌宏
富士通研究所人工知能研究部
-
藤田 昌宏
東京大学大学院工学系研究科電子工学
-
松本 剛史
東京大学大規模集積システム設計教育研究センター
-
藤田 昌宏
東京大学大規模集積システム設計教育研究センター:科学技術振興機構戦略的創造研究推進事業crest
-
藤田 昌宏
埼玉大学大学院理工学研究科
-
藤田 昌宏
東京大学大規模集積システム設計教育研究センター
-
藤田 昌宏
国立札幌病院
-
藤田 昌宏
東京大学大規模集積システム設計教育研究センター(vdec)|科学技術振興機構戦略的創造研究推進事業crest
-
藤田 昌宏
富士通研
-
藤田 昌宏
東京大学、大規模集積システム設計教育研究センター
-
藤田 昌宏
東京大学大規模集積システム設計教育研究センター|科学技術振興機構戦略的創造研究推進事業crest
-
李 在城
東京大学大学院工学系研究科電気系工学専攻
-
藤田 昌宏
東京大学大規模集積システム設計教育研究センター(VDEC):科学技術振興機構戦略的創造研究推進事業CREST
関連論文
- A method of reproducing input/output error trace on high-level design for hardware debug support (ディペンダブルコンピューティング)
- TA-1-3 高位検証技術の基礎
- 「システムLSIの設計技術と設計自動化」の編集にあたって
- 算術演算回路のデバッグ支援技術
- SpecC言語に基づくシステムレベル設計手法
- LSIの設計品質はCADツールの使いこなしが決める! : CAD技術の研究開発なくして高性能LSIはない
- 問題点のまとめと1つの提案
- システムLSIの設計技術・設計支援技術(CAD技術)に関する問題点
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ (画像工学)
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ (集積回路)
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ (信号処理)
- 設計再利用のためのIPライブラリ検索システム(上流設計技術(1),システムオンシリコン設計技術並びにこれを活用したVLSI)
- SATアルゴリズムの最新動向
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバック,組込技術とネットワークに関するワークショップETNET2009)
- 上位設計記述におけるダイナミックプログラムスライシングを用いたポストシリコンデバッグ支援手法(デバッグ,組込技術とネットワークに関するワークショップETNET2009)
- 専用プロセッサ用命令セットの自動生成手法の提案と実装
- ハードウェアデバッグ支援のためのエラー入出力トレースの上位レベル設計における再現手法(高位レベルテスト・検証,VLSI設計とテスト及び一般)
- 準形式的モデル検査のハードウェア実装による高速化の検討(モデル・回路,組込技術とネットワークに関するワークショップETNET2008)
- 算術演算回路のデバッグ支援技術
- SpecC言語に基づくシステムレベル設計手法
- SpecC言語に基づくシステムレベル設計手法
- Performance-Constrained Transistor Sizing for Different Cell Count Minimization
- AI-1-4 超ディペンダブルVLSIへの挑戦(AI-1.デイベンダブルVLSIに向けて,依頼シンポジウム,ソサイエティ企画)
- 製造後デバッグのための入出力シーケンススライシング手法(設計/テスト/検証)
- Synchronization Verification in System-Level Design with ILP Solvers(System Level Design,VLSI Design and CAD Algorithms)
- 電子系・機械系協調設計における設計検証法に関する検討(実時間処理,組込システム及び一般)
- 電子系・機械系協調設計における設計検証法に関する検討(実時間処理,組込システム及び一般)
- 充足可能性判定に基づくシステムレベルデバッグ支援手法におけるバグモデルの導入による効率化
- 上位設計記述の解析を利用した製造後機能テストの効率化
- 動的パッチ読み出し機構を備えた製造後機能修正可能アクセラレータ
- EFSM-based Weight-oriented Concolic Testing for Embedded Software
- 依存グラフを用いた局所的な記号シミュレーションによるC言語記述に対する等価性検証手法の提案(システムLSI設計及び一般)
- 依存グラフを用いた局所的な記号シミュレーションによるC言語記述に対する等価性検証手法の提案(システムLSI設計及び一般)
- C言語を対象とした記述間の差異に基づく効率的な等価性検証手法(システムオンシリコン設計技術並びにこれを活用したVLSI)
- C言語を対象とした記述間の差異に基づく効率的な等価性検証手法(システムオンシリコン設計技術並びにこれを活用したVLSI)
- C言語でのハードウェア記述に対する効率的な等価性検証手法の提案(システム設計及び一般)
- C言語でのハードウェア記述に対する効率的な等価性検証手法の提案(システム設計及び一般)
- ループ融合を利用した複数のforループからのパイプラインハードウェア合成
- ループ融合を利用した複数の for ループからのパイプラインハードウェア合成
- 1M-5 ワードレベル論理式の充足可能性判定問題を利用したシステムレベル設計デバッグ支援手法(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 潜在的多様性を考慮したプログラマブルハードウェアの高位合成手法(プログラマブルデバイスと設計技術,システムオンシリコンを支える設計技術)
- 設計固有セルライブラリの自動生成手法(論理設計,デザインガイア2009-VLSI設計の新しい大地)
- 仮想マルチプロセッサモデルに基づく高速SoCプロトタイピング手法(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 仮想マルチプロセッサモデルに基づく高速SoCプロトタイピング手法(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 高性能SoCプロトタイプのFPGA実装方式の検討(論理設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 高性能SoCプロトタイプのFPGA実装方式の検討(論理設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 上位設計記述の解析を利用した製造後機能テストの効率化 (ディペンダブルコンピューティング)
- 上位設計記述の解析を利用した製造後機能テストの効率化 (VLSI設計技術)
- RTL-Tokioに基づくパイプライン化支援
- RTL-Tokio : レジスタトランスファレベル動作記述言語
- 時相論理型言語Tokioによる論理回路検証系の評価
- 時相論理型言語Tokioによるハードウェア記述 : 時間に依存するfactによる同期記述
- 1M-6 動作合成された束データ方式による非同期式回路とその動作仕様に対する等価性検証手法(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 2分決定グラフを用いた推移的閉包計算アルゴリズムと形式的検証への応用
- Boolean Relationからの多段論理回路の合成
- 2. 形式的検証手法の実設計への適用例 ( 論理設計の形式的検証)
- 特集「論理設計の形式的検証」の編集にあたって
- VLSI実設計に於ける形式的検証の適用
- 多入力論理関数に対する効率的なWalshスペクトルの計算手法とそのテクノロジマッピングへの応用
- チャネル境界上の端子位置決定法
- Rectangular Dualに基づくマクロセル配置手法
- 多段論理合成における二段論理式簡単化の一手法
- 順序付き2分決定グラフと許容関数を用いた多段論理回路簡単化手法 (回路自動合成と最適化論文特集)
- 大規模回路の多段論理簡単化について
- 順序回路の簡単化について
- 遅延を意識したレジスタトランスファレベルからの合成について
- 2分決定グラフのための変数順決定アルゴリズムとその評価
- 遅延時間の増加を押さえたトランスダクション法について
- トランスダクション法に基づく多段論理回路簡単化機能をもつ論理合成システム
- 2分決定グラフを利用したトランスダクション法の改良
- 時相論理による仕様記述支援システム
- グラフに基づく論理照合アルゴリズムの評価と改良
- 論理とそのVLSI設計への応用 (VLSI設計の新しい流れ)
- 発見的手法に基づくスケーラブルなインクリメンタル高位合成(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 発見的手法に基づくスケーラブルなインクリメンタル高位合成(高位設計1,デザインガイア2010-VLSI設計の新しい大地-)
- 2P-1 動的ウェブアプリケーションの操作に対する画面間遷移の網羅的検証(ソフトウェアの検査・検証,学生セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- インクリメンタル高位合成に向けた設計記述間差分の計算手法 (ディペンダブルコンピューティング)
- インクリメンタル高位合成に向けた設計記述間差分の計算手法 (コンピュータシステム)
- システムレベル設計における同期検証フレームワークの提案
- システムレベル設計における同期検証フレームワークの提案
- データ符号化によるVLSIにおける低消費電力・高信頼データ伝送手法の検討
- データ符号化によるVLSIにおける低消費電力・高信頼データ伝送手法の検討(低消費)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会)
- トランスダクション法に基づく多段論理回路簡単化機能をもつ論理合成システムとその評価
- 時相論理型言語Tokioを利用したハードウェア機能設計
- インクリメンタル高位合成に向けた設計記述間差分の計算手法
- インクリメンタル高位合成に向けた設計記述間差分の計算手法
- FPGAを用いたSmith-Waterman Algorithmの高速化(科学技術計算)
- 高位合成ツールを利用したハードウェアアルゴリズムの最適化(最適化技術,システム設計及び一般)
- 反例と設計分割に基づく高位設計に対する効率的な設計修正支援手法(検証技術,システム設計及び一般)
- 形式的検証を用いたプロセッサエラー回復機構の耐性評価手法の検討(検証技術,システム設計及び一般)
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討
- ゲート回路シミュレーションにおけるGPGPUを利用したアサーション自動抽出
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討(設計技術,組込み技術とネットワークに関するワークショップETNET2012)
- 論理関数の充足不可能性に注目した論理回路デバッグ手法の検討(設計技術,組込み技術とネットワークに関するワークショップETNET2012)
- 動作レベル・レジスタ転送レベル混在設計記述向け高位合成手法(動作レベル設計と配線手法,システムオンシリコンを支える設計技術)
- 潜在的な依存関係を利用した高位設計デバッグ支援手法(システム設計,システム設計及び一般)
- 誤差を有するシステムのシミュレーション結果に対する統計的解析とそのハードウェアによる高速化(設計環境,システム設計及び一般)
- プログラム可能な素子を利用したゲートレベル回路のデバッグ手法
- プログラム可能な素子を利用した大規模回路の自動修復手法