講演抄録/キーワード |
講演名 |
2014-06-12 16:00
FPGAを用いた可変連想度セットアソシエイティブキャッシュによる充足/最大充足可能性問題の高速計算 ○金澤健治・丸山 勉(筑波大) RECONF2014-14 |
抄録 |
(和) |
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 / / / / |
文献情報 |
信学技報, vol. 114, no. 75, RECONF2014-14, pp. 73-78, 2014年6月. |
資料番号 |
RECONF2014-14 |
発行日 |
2014-06-04 (RECONF) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
RECONF2014-14 |
研究会情報 |
研究会 |
RECONF |
開催期間 |
2014-06-11 - 2014-06-12 |
開催地(和) |
片平さくらホール |
開催地(英) |
Katahira Sakura Hall |
テーマ(和) |
リコンフィギャラブルシステム、一般 |
テーマ(英) |
Reconfigurable Systems, etc. |
講演論文情報の詳細 |
申込み研究会 |
RECONF |
会議コード |
2014-06-RECONF |
本文の言語 |
日本語 |
タイトル(和) |
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 |
キーワード(5)(和/英) |
/ |
キーワード(6)(和/英) |
/ |
キーワード(7)(和/英) |
/ |
キーワード(8)(和/英) |
/ |
第1著者 氏名(和/英/ヨミ) |
金澤 健治 / Kenji Kanazawa / カナザワ ケンジ |
第1著者 所属(和/英) |
筑波大学 (略称: 筑波大)
University of Tsukuba (略称: Univ. of Tsukuba) |
第2著者 氏名(和/英/ヨミ) |
丸山 勉 / Tsutomu Maruyama / |
第2著者 所属(和/英) |
筑波大学 (略称: 筑波大)
University of Tsukuba (略称: Univ. of Tsukuba) |
第3著者 氏名(和/英/ヨミ) |
/ / |
第3著者 所属(和/英) |
(略称: )
(略称: ) |
第4著者 氏名(和/英/ヨミ) |
/ / |
第4著者 所属(和/英) |
(略称: )
(略称: ) |
第5著者 氏名(和/英/ヨミ) |
/ / |
第5著者 所属(和/英) |
(略称: )
(略称: ) |
第6著者 氏名(和/英/ヨミ) |
/ / |
第6著者 所属(和/英) |
(略称: )
(略称: ) |
第7著者 氏名(和/英/ヨミ) |
/ / |
第7著者 所属(和/英) |
(略称: )
(略称: ) |
第8著者 氏名(和/英/ヨミ) |
/ / |
第8著者 所属(和/英) |
(略称: )
(略称: ) |
第9著者 氏名(和/英/ヨミ) |
/ / |
第9著者 所属(和/英) |
(略称: )
(略称: ) |
第10著者 氏名(和/英/ヨミ) |
/ / |
第10著者 所属(和/英) |
(略称: )
(略称: ) |
第11著者 氏名(和/英/ヨミ) |
/ / |
第11著者 所属(和/英) |
(略称: )
(略称: ) |
第12著者 氏名(和/英/ヨミ) |
/ / |
第12著者 所属(和/英) |
(略称: )
(略称: ) |
第13著者 氏名(和/英/ヨミ) |
/ / |
第13著者 所属(和/英) |
(略称: )
(略称: ) |
第14著者 氏名(和/英/ヨミ) |
/ / |
第14著者 所属(和/英) |
(略称: )
(略称: ) |
第15著者 氏名(和/英/ヨミ) |
/ / |
第15著者 所属(和/英) |
(略称: )
(略称: ) |
第16著者 氏名(和/英/ヨミ) |
/ / |
第16著者 所属(和/英) |
(略称: )
(略称: ) |
第17著者 氏名(和/英/ヨミ) |
/ / |
第17著者 所属(和/英) |
(略称: )
(略称: ) |
第18著者 氏名(和/英/ヨミ) |
/ / |
第18著者 所属(和/英) |
(略称: )
(略称: ) |
第19著者 氏名(和/英/ヨミ) |
/ / |
第19著者 所属(和/英) |
(略称: )
(略称: ) |
第20著者 氏名(和/英/ヨミ) |
/ / |
第20著者 所属(和/英) |
(略称: )
(略称: ) |
講演者 |
第1著者 |
発表日時 |
2014-06-12 16:00:00 |
発表時間 |
25分 |
申込先研究会 |
RECONF |
資料番号 |
RECONF2014-14 |
巻番号(vol) |
vol.114 |
号番号(no) |
no.75 |
ページ範囲 |
pp.73-78 |
ページ数 |
6 |
発行日 |
2014-06-04 (RECONF) |
|