論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法(検証)
スポンサーリンク
概要
- 論文の詳細を見る
本稿では、SATを用いた論理回路の形式的検証の高速化を目指し、論理回路からSAT-solverの実行時間が短かくなるような和積標準形CNF論理式を生成する、CNF式生成処理フレームワークを提案する。提案するフレームワークは、回路分割と、部分回路のBDD生成、BDDからCNF式への変換から構成される。また本稿では、提案フレームワークに基づく、中間変数の間隔を考慮した回路分割、BDD生成、BDDからCNF式への変換アルゴリズムを示す。提案するCNF式生成手法と広く用いられているCNF式生成手法を実装し、SAT-solverの実行時間について比較を行ったところ、提案手法により実行時間が短縮されることが確認された。
- 一般社団法人情報処理学会の論文
- 2007-03-15
著者
-
成瀬 智啓
名古屋大学大学院情報科学研究科
-
中村 一博
名古屋大学大学院情報科学研究科
-
高木 一義
名古屋大学大学院情報科学研究科
-
高木 直史
名古屋大学大学院情報科学研究科
-
高木 一義
名古屋大学
-
高木 直史
名古屋大学
-
中村 一博
名古屋大学
関連論文
- Nbアドバンストプロセスを用いた単一磁束量子浮動小数点演算器の設計(ディジタル,一般)
- SFQ半精度浮動小数点乗算器の設計と試作(デジタル,一般)
- 投票無衝突化手法を用いた小面積画素並列ハフ変換回路(応用,組込技術とネットワークに関するワークショップETNET2009)
- SFQ半精度浮動小数点加算器の設計と試作(デジタル,一般)
- C-8-10 SFQ浮動小数点乗算器の同期化および動作実証(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-13 Nb多層プロセスを用いて試作したシフトレジスタの測定評価(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-7 超伝導SFQ回路のための新Nb多層プロセス(C-8. 超伝導エレクトロニクス,一般セッション)
- Nb多層デバイス構造用セルライブラリに向けた最適なモート構造の検討(単一磁束量子大規模集積回路技術の現状と将来展望、デジタル応用及び一般)
- パイプライン動作を考慮した単一磁束量子回路のための論理設計検証手法(ディジタル,一般)
- トランスダクション法に基づく単一磁束量子回路合成のためのフレームワーク
- 投票高々1衝突化手法を用いた小面積画素並列ハフ変換回路の設計 (ディペンダブルコンピューティング)
- 投票高々1衝突化手法を用いた小面積画素並列ハフ変換回路の設計 (VLSI設計技術)
- TLDP法のパイプライン化による省メモリな連続単語音声認識回路 (集積回路)
- A-3-1 Sequential SATの高速化のためのm-Trieを用いた時間フレームを跨いだ状態併合(A-3.VLSI設計技術,一般セッション)
- C-8-14 可変遅延素子を用いた単一磁束量子可変長シフトレジスタ(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-9 A^*アルゴリズムに基づく単一磁束量子回路受動線路配線ツールの実装と評価(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-12 SFQ半精度浮動小数点乗算器の試作と動作実証(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-18 SFQ半精度浮動小数点乗算器の設計と試作(C-8. 超伝導エレクトロニクス,一般セッション)
- C-8-15 10kA/cm^2Nbアドバンスドプロセスを用いたSFQ半精度浮動小数点乗算器の設計(C-8.超伝導エレクトロニクス,一般セッション)
- A-20-20 TLDP法の並列化による省メモリな連続単語音声認識回路(A-20. スマートインフォメディアシステム,一般セッション)
- C-8-5 10kA/cm^2Nbプロセスを用いたSFQ半精度浮動小数点加算器のコンポーネント回路の設計(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-2 単一磁束量子回路による冗長2進表現を用いたシストリックシリアル指数計算回路(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-1 単一磁束量子回路のためのパイプライン検証手法(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-13 SFQ回路のためのレイアウトを考慮したスキューのあるクロック木の構成法(C-8.超伝導エレクトロニクス,一般セッション)
- 平方根の逆数計算回路の設計と評価
- 平方根の逆数計算回路の設計と評価
- 平方根の逆数計算回路の設計と評価
- Steinのアルゴリズムに基づく有限体上の除算アルゴリズム
- Steinのアルゴリズムに基づく有限体上の除算アルゴリズム
- Steinのアルゴリズムに基づく有限体上の除算アルゴリズム
- 投票高々1衝突化手法を用いた小面積画素並列ハフ変換回路の設計
- 再構成可能なデータパスに向けた単一磁束量浮動小数点除算器の実証(単一磁束量子大規模集積回路技術の現状と将来展望、デジタル応用及び一般)
- C-8-22 単一磁束量子回路のフロアプラン設計支援に向けた配線遅延時間の推定(C-8. 超伝導エレクトロニクス,一般セッション)
- C-8-10 シストリックアーキテクチャに基づく高スループットSFQビットシリアル浮動小数点乗算器(C-8.超伝導エレクトロニクス,一般講演)
- C-8-9 単一磁束量子回路による冗長2進表現を用いたシストリック開平器の設計(C-8.超伝導エレクトロニクス,一般講演)
- C-8-11 冗長2進表現を用いたシストリックSFQ除算器(C-8.超伝導エレクトロニクス,一般講演)
- A-3-10 単一磁束量子ディジタル回路のためのone-hot状態割り当てを用いた順序回路の構成法(A-3.VLSI設計技術,一般講演)
- C-8-15 トルネードアーキテクチャに基づく単一磁束量子マイクロプロセッサのALUの改善(C-8.超伝導エレクトロニクス,一般講演)
- C-8-12 トルネードアーキテクチャにおけるSFQマイクロプロセッサのデータパスの動作実証(C-8.超伝導エレクトロニクス,一般講演)
- C-8-10 トルネードアーキテクチャにおけるSFQマイクロプロセッサのデータパスの設計(C-8.超伝導エレクトロニクス,エレクトロニクス2)
- C-8-9 クロック同期式SFQ回路のクロック木合成(C-8.超伝導エレクトロニクス,エレクトロニクス2)
- C-8-5 SFQマイクロプロセッサに向けたレジスタファイルの実証(C-8. 超伝導エレクトロニクス, エレクトロニクス2)
- SC-8-11 単一磁束量子マイクロプロセッサの開発(SC-8.超伝導SFQ回路技術の最近の進展)
- C-8-12 SFQマイクロプロセッサに向けたトルネードアーキテクチャの提案(C-8.超伝導エレクトロニクス)
- 順序回路の形式的検証におけるフォールスネガティブ削減のための回路変換(システム設計・高位論理設計,システムオンシリコンを支える設計技術)
- C-8-4 SFQ回路実現に向いた直並列型2の補数乗算器(C-8. 超伝導エレクトロニクス, エレクトロニクス2)
- C-8-10 SFQマイクロプロセッサに用いるコンパレータの設計(C-8.超伝導エレクトロニクス)
- 多層配線単一磁束量子回路のための自動配線手法(単一磁束量子大規模集積回路技術の現状と将来展望、デジタル応用及び一般)
- 保存型一括並列処理による高速なHMM出力確率計算・最尤推定回路の構成法
- 保存型一括並列処理による高速なHMM出力確率計算・最尤推定回路の構成法
- 保存型一括並列処理による高速なHMM出力確率計算・最尤推定回路の構成法
- 保存型一括並列処理による高速なHMM出力確率計算・最尤推定回路の構成法
- 単一磁束量子論理回路のための故障モデルとテストパターン生成手法の検討(信号処理基盤技術及びその応用,一般)
- A fast VLSI architecture of output probability computations and Viterbi scorer for HMM-based recognition systems with store-based block parallel processing (ディペンダブルコンピューティング)
- A fast VLSI architecture of output probability computations and Viterbi scorer for HMM-based recognition systems with store-based block parallel processing (コンピュータシステム)
- バイアス電源の高電圧化による単一磁束量子回路の高速化の検討(信号処理基盤技術及びその応用,一般)
- 再構成可能部を持つJavaプロセッサにおけるハードウェアJIT機構の検討
- 再構成可能部を持つJavaプロセッサにおけるハードウェアJIT機構の検討
- A-3-16 再構成可能部を持つJavaプロセッサにおける高速化方式およびハードウェアJIT方式の検討
- 10kA/cm^2Nb Processを用いたSFQ浮動小数点乗算器の50GHzでの動作評価(信号処理基盤技術及びその応用,一般)
- C-8-15 10kA/cm^2Nb Processを用いたSFQ浮動小数点乗算器コンポーネント回路の動作評価(C-8.超伝導エレクトロニクス,一般セッション)
- C-8-14 10kA/cm^2Nbプロセスを用いたSFQ半精度浮動小数点加算器のコンポーネント回路の動作実証(C-8.超伝導エレクトロニクス,一般セッション)
- 加算器の平均スイッチングエネルギーの解析的評価(低電力設計と回路設計技術,システムオンシリコンを支える設計技術)
- C-8-16 大規模単一磁束量子回路向け動的消費エネルギ計算ツールの検討(C-8.超伝導エレクトロニクス,一般セッション)
- 乗算器および除算器IPの開発
- 保存型一括並列処理による高速なHMM出力確率計算・最尤推定回路の構成法
- 保存型一括並列処理による高速なHMM出力確率計算・最尤推定回路の構成法
- 保存型一括並列処理による高速なHMM出力確率計算・最尤推定回路の構成法
- 保存型一括並列処理による高速なHMM出力確率計算・最尤推定回路の構成法
- セル遅延モデルを用いた算術演算回路の信号遷移回数見積もり手法(システム設計・高位論理設計,システムオンシリコンを支える設計技術)
- TLDP法のパイプライン化による省メモリな連続単語音声認識回路
- TLDP法のパイプライン化による省メモリな連続単語音声認識回路
- TLDP法のパイプライン化による省メモリな連続単語音声認識回路
- 二段階検証による順序回路の限定モデル検査の高速化手法 (VLSI設計技術)
- 多重高速保存型一括並列処理による省メモリな音声認識用HMM計算回路 (ディペンダブルコンピューティング)
- 多重高速保存型一括並列処理による省メモリな音声認識用HMM計算回路 (コンピュータシステム)
- A-3-6 Sequential SATにおける時間フレームを跨いだ状態併合(A-3.VLSI設計技術,一般セッション)
- 論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法(検証)
- 論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法(検証)
- 論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法(検証,組込技術とネットワークに関するワークショップETNET2007)
- 論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法(検証,組込技術とネットワークに関するワークショップETNET2007)
- 部分積加算における信号遷移回数の削減による配列型乗算器の低消費エネルギー化設計(消費電力2,デザインガイア2007-VLSI設計の新しい大地を考える研究会-)
- 部分積加算における信号遷移回数の削減による配列型乗算器の低消費エネルギー化設計(消費電力2,デザインガイア2007-VLSI設計の新しい大地を考える研究会-)
- 部分積加算における信号遷移回数の削減による配列型乗算器の低消費エネルギー化設計(消費電力2,デザインガイア2007-VLSI設計の新しい大地を考える研究会-)
- A-3-13 次元数とフレーム数の変化に対応可能なHMM回路(A-3. VLSI設計技術)
- A-20-1 投票無衝突化と投票空間アクセス局所化による小面積画素並列ハフ変換回路(A-20.スマートインフォメディアシステム,一般セッション)
- 多重高速保存型一括並列処理による省メモリな音声認識用HMM計算回路
- 多重高速保存型一括並列処理による省メモリな音声認識用HMM計算回路
- 投票無衝突化手法を用いた小面積画素並列ハフ変換回路(応用,組込技術とネットワークに関するワークショップETNET2009)
- 投票無衝突化手法を用いた小面積画素並列ハフ変換回路(応用,組込技術とネットワークに関するワークショップETNET2009)
- 投票無衝突化手法を用いた小面積画素並列ハフ変換回路(応用,組込技術とネットワークに関するワークショップETNET2009)
- 投票メモリへのアクセスを局所化した並列ハフ変換回路の構成法(応用,組込技術とネットワークに関するワークショップETNET2008)
- 投票メモリへのアクセスを局所化した並列ハフ変換回路の構成法(応用,組込技術とネットワークに関するワークショップETNET2008)
- 投票メモリへのアクセスを局所化した並列ハフ変換回路の構成法(応用,組込技術とネットワークに関するワークショップETNET2008)
- 投票メモリへのアクセスを局所化した並列ハフ変換回路の構成法(応用,組込技術とネットワークに関するワークショップETNET2008)
- セル遅延モデルを用いた算術演算回路の信号遷移回数見積もり手法
- 二段階検証による順序回路の限定モデル検査の高速化手法(論理設計2,システムオンシリコンを支える設計技術)
- A-3-14 省メモリ型HMM回路(A-3. VLSI設計技術)
- A-3-8 順序回路の形式的検証のための1-hotカウンタ検出手法(A-3.VLSI設計技術,一般講演)
- A-3-3 2の補数乗算器に対応した加算ネットワークの抽出手法(A-3.VLSI設計技術,一般講演)