LUT回路のブーリアンマッチング手法について

摘要

本稿では複数のLUTからなる回路が与えられた論理関数を実現できるかどうかを調べるブーリアンマッチングの高速化手法について述べる．高速化手法は2つある．1つは入力順序の割り当てをone-hot符号化された変数を用いて表す手法であり，従来の2進符号化に比べると必要となる変数の数は増えるが，ほとんどの制約が2項節の形で与えられるため，SATソルバにおいて効率的な値の伝搬が行える．もう1つは段階的探索手法で，マッチングが失敗する例において，部分的な制約式のみを評価することで早めに充足不能と判定を行い，無駄な探索を省いている．充足可能となる場合でも以前の評価の結果得られた学習節が後の評価の際にも用いられるのでオーバーヘッドは少ない．