| 研究概要 |
命題論理の充足性判定器(SATソルバ)をFPGA上に試作し,従来ソフトウェア実装しかなかった記号処理の分野においても,再構成可能な演算チップの利用により高性能なハードウェア実装が可能であることを実証した.また,SATソルバのシミュレータをJavaを用いて試作し,再構成可能な演算チップを利用するシステムの開発をソフトウェア面で支援する技術と環境に関する検討と整備を進めた.
SATソルバは3通りの方式で実装し,ベンチマーク問題を用いて比較評価を行なった.各方式とも問題ごとに回路を再構成するもので,論理セル数5万個強のFPGA上に最大で変数100個,節数200本の問題が実装できた.基本推論については,各節の充足性判定を同時並行的に行なう構成により,ソフトウェアに比べて数100倍の速度向上が得られた.ソフトウェア実装において通常行なわれる補題生成や知的後戻りについては,極めて限定的な手法を採用したにも関わらず,著しい探索空間の絞込み効果により,問題によっては数1000倍以上の高速化が得られた.変数順序の変更等の探索ヒューリスティックスについても,同様に問題依存ではあるが,顕著な効果が認められた.
シミュレータについては,Verilog-HDLの記述とほぼ1対1のJava記述を行える方式を考案した.Verilog-HDL記述が並行処理的ながらもあくまで同期回路を前提としているため,逐次処理に基づく本方式のJava記述において,信号の依存関係さえ正しく保てば組み合わせ回路,順序回路ともに論理的機能を容易に模擬できる.実際,本シミュレータの利用により,多大な再構成時間を要するFPGA実装の設計,デバッグ工程を著しく短縮,省力化できた.
|
