@techreport{oai:ipsj.ixsq.nii.ac.jp:00240525, author = {松永, 裕介 and Yusuke, Matsunaga}, issue = {43}, month = {Nov}, note = {本稿では SAT ソルバを用いてテストパタン生成を行うための故障検出条件のコンパクトな表現方法について提案を行う.著者は外部入力に加えて内部の信号線を含めたブール空間上でのキューブ (積項) を用いて故障の検出条件を表す手法を提案している.多くの場合,一つの故障に対して必要となる積項数は数個以下であり,効率の良い表現方法と言えるが,故障によっては数 100 個の積項を用いても完全な故障検出条件を表せない場合もある.そこで,多数の積項を必要とする場合の故障検出条件を一旦 BDD に変換し,BDD の構造を再度 CNF 式に変換することでより小さなサイズの論理式を生成する手法を提案する.ベンチマーク回路を用いた実験では,元の論理式の積項数が多い場合には BDD を用いた手法のほうがよりコンパクトな表現を得られることが示されている., This paper presents a novel methd for concisely representing the condition of fault detection, which is assumed to be used for test pattern generation with SAT solver. The author proposed a method for representing the condition of fault detection, which uses cubes(product terms) of extented Boolean space over the external inputs with addition to the internal signals. In many cases, the number of cubes required for representing the fault detect conditions is very few, howerver, there are cases such that even handreds of cubes cannot represent the fault detect condition completely. To represent the condition concisely for such cases, this paper proposes a new method to generate a logic formula representing the fault detect condition. The proposed method first construct a BDD which represents the given fault detect condition, then it converts the BDD structure to CNF formula. With experiments using benchmark circuits, the proposed method is able to represent the fault detect condition concisely for the cases whose number cubes are more than handreds.}, title = {SATソルバを用いたテスト生成手法用の故障検出条件の表現方法}, year = {2024} }