| 講演名 | 2014-06-12 FPGAを用いた可変連想度セットアソシエイティブキャッシュによる充足/最大充足可能性問題の高速計算(アプリケーション高速化) 金澤 健治, 丸山 勉, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | WSATアルゴリズムは,充足可能性問題(SAT)および最大充足可能性問題(MaxSAT)の解法のひとつであり,その並列度の高さから,ハードウェア化に適している.形式検証問題は,SATおよびMaxSATの重要な応用問題であるが,その規模はFPGAのオンチップメモリと比較して非常に大きく,ハードウェアの性能はデータを保持するDRAMのデータ転送速度により制限される.本稿では,FPGAのオンチップメモリを利用した可変連想度キャッシュにより,DRAMアクセス遅延を隠蔽する手法を提案する.評価の結果,DRAMアクセス遅延のうち最大60%を隠蔽することが可能であり,キャッシュを行わない場合と比較して,最大26%の速度向上が可能であった. |
| 抄録(英) | WalkSAT (WSAT) is one of the stochastic local search algorithms for Boolean Satisfiability (SAT) and Maximum Boolean Satisfiability (MaxSAT), and it is very suitable for hardware acceleration, because of its high inherent parallelism. Formal verification is one of the most important applications of SAT and MaxSAT, however, the size of the formal verification problems is significantly larger than on-chip memory size, and most of the data have to be placed in off-chip DRAM. In this approach, however, the acceleration was still limited by the DRAM access delay. In this paper, we propose a method to hide the access delay by using on-chip memory banks as a variable-way associative cache memory. With this cache memory, up to 60% DRAM access delay can be hidden, and the performance can be improved up to 26%. |
| キーワード(和) | FPGA / SAT / MaxSAT / WSAT |
| キーワード(英) | FPGA / SAT / MaxSAT / WSAT |
| 資料番号 | RECONF2014-14 |
| 発行日 |
| 研究会情報 | |
| 研究会 | RECONF |
|---|---|
| 開催期間 | 2014/6/4(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Reconfigurable Systems (RECONF) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | FPGAを用いた可変連想度セットアソシエイティブキャッシュによる充足/最大充足可能性問題の高速計算(アプリケーション高速化) |
| サブタイトル（和） | |
| タイトル（英） | FPGA Acceleration of SAT/MaxSAT Solving using Variable-way Set Associative Cache |
| サブタイトル（和） | |
| キーワード(1)（和/英） | FPGA / FPGA |
| キーワード(2)（和/英） | SAT / SAT |
| キーワード(3)（和/英） | MaxSAT / MaxSAT |
| キーワード(4)（和/英） | WSAT / WSAT |
| 第 1 著者 氏名（和/英） | 金澤 健治 / Kenji KANAZAWA |
| 第 1 著者 所属（和/英） | 筑波大学システム情報系情報工学域 Faculty of, University of Tsukuba |
| 第 2 著者 氏名（和/英） | 丸山 勉 / Tsutomu MARUYAMA |
| 第 2 著者 所属（和/英） | 筑波大学システム情報系知能機能工学域 Division of Intelligent Interaction Technologies, Faculty of Systems and Information Engineering, University of Tsukuba |
| 発表年月日 | 2014-06-12 |
| 資料番号 | RECONF2014-14 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | 75 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |