FPGAを用いた可変連想度セットアソシエイティブキャッシュによる充足／最大充足可能性問題の高速計算

摘要

WSATアルゴリズムは，充足可能性問題（SAT）および最大充足可能性問題（MaxSAT）の解法のひとつであり，その並列度の高さから，ハードウェア化に適している．形式検証問題は，SATおよびMaxSATの重要な応用問題であるが，その規模はFPGAのオンチップメモリと比較して非常に大きく，ハードウェアの性能はデータを保持するDRAMのデータ転送速度により制限される．本稿では，FPGAのオンチップメモリを利用した可変連想度キャッシュにより，DRAMアクセス遅延を隠蔽する手法を提案する．評価の結果，DRAMアクセス遅延のうち最大60％を隠蔽することが可能であり，キャッシュを行わない場合と比較して，最大26％の速度向上が可能であった．