論理関数の充足不可能性に注目した論理回路デバッグ手法の検討

スポンサーリンク

概要

論文の詳細を見る
回路中の誤り箇所を特定するデバッグは時間のかかる作業である。従来手法では反例に基づいてデバッグを始めるが、本稿では反例が得られない状況におけるデバッグ方法を考える。論理関数の充足可能性 (SAT) 問題を用いた検証では、充足可能な場合に設計が正しくなるように定式化される場合、反例を特定することができない。この場合には、論理式中で矛盾を起こしている部分集合 (UNSAT コア) がデバッグのヒントになると考えられる。そこで本稿では、複数の UNSAT コアを用いることで、誤り候補を絞り込む手法を考える。しかし、UNSAT コアを多数求めようとすると、現在のアルゴリズムでは計算量が爆発的に増加し、このままでは使えないという問題がある。本稿では、簡単な回路を対象に上記の方法を説明し、問題点を克服するための考察を行う。
2012-02-24

著者

関連論文

もっと見る

スポンサーリンク