プログラム可能データパスとSMTソルバーを利用した高位設計デバッグ手法

摘要

近年、Look-up Table （LUT）のようなプログラム可能回路を利用した論理回路の自動デバッグ手法が提案されている。この手法では、回路中にLUTを挿入し、SATソルバーを用いて、回路が仕様を満たすようなLUTの論理定義を求めることによって論理修正を行う。この考え方は、LUTの代わりにUninterpreted Function （UIF）を利用することによって、ワード変数とそれらに対する演算が記述される高位設計に適用することができる。この場合、SATソルバーの代わりに、ワード変数や算術演算を含む論理式のSAT問題を効率良く解くことができるSMTソルバーが使われる。しかし、一般的に、UIFを利用した手法においては、得られた誤り修正の解を限られた種類の利用可能な演算（器）で実現することは容易ではない。そこで、UIFではなく、プログラム可能なデータパスを利用することにより、利用可能な演算によって実装可能な誤り修正を求める手法を提案する。提案するプログラム可能データパスでは、与えられた演算を最大N回まで適用する任意のデータパスが表現可能であり（Nは指定された数）、その中に仕様を満たす構成が含まれるかをSMTソルバーで解く。いくつかの例題に対して、仕様を満たすプログラム可能データパスの構成を求める実験を行い、その性能を評価する。