2024-03-29T20:09:01Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000808972024-03-29T05:26:34Z01164:02822:06703:06704
論理関数の充足不可能性に注目した論理回路デバッグ手法の検討A consideration of logical circuit debugging method using unsatisfiabilityjpn設計技術http://id.nii.ac.jp/1001/00080897/Technical Reporthttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=80897&item_no=1&attribute_id=1&file_no=1Copyright (c) 2012 by the Information Processing Society of Japan東京大学大学院工学系研究科電気系工学専攻東京大学大規模集積システム設計教育研究センター東京大学大規模集積システム設計教育研究センター/科学技術振興機構戦略的創造研究推進事業CREST李, 在城松本, 剛史藤田, 昌宏回路中の誤り箇所を特定するデバッグは時間のかかる作業である。従来手法では反例に基づいてデバッグを始めるが、本稿では反例が得られない状況におけるデバッグ方法を考える。論理関数の充足可能性 (SAT) 問題を用いた検証では、充足可能な場合に設計が正しくなるように定式化される場合、反例を特定することができない。この場合には、論理式中で矛盾を起こしている部分集合 (UNSAT コア) がデバッグのヒントになると考えられる。そこで本稿では、複数の UNSAT コアを用いることで、誤り候補を絞り込む手法を考える。しかし、UNSAT コアを多数求めようとすると、現在のアルゴリズムでは計算量が爆発的に増加し、このままでは使えないという問題がある。本稿では、簡単な回路を対象に上記の方法を説明し、問題点を克服するための考察を行う。Detecting errorneous behaviors in logic circuits and debugging are time-consuming tasks in circuit designs. While there exist many debugging methodologies starting with counter-examples, we consider to debug circuits when the circuits have no or few counter-examples. When a verification problem is formulated as Boolean satisfiability, a variable assignment generated by SAT solvers is a counter-example, when the formula is set to be false if the circuit behavior is correct. On the other hand, we can formulate a verification problem so that the Boolean formula is true if the circuit behavior is correct. In the case, we can find hints for debugging in UNSAT cores which are subsets of caluses including a logical conflict inside, since UNSAT cores correspond to a part of the circuit which has a logical conflict to the verified property. In this work, we consider to locate bugs using an intersection of multiple UNSAT cores for a property. However, the computation to get UNSAT cores exponentially increases with the number of UNSAT cores. In this paper, we discuss circuit debugging with UNSAT cores and more efficient ways to get UNSAT cores.AA12149313研究報告組込みシステム(EMB)2012-EMB-245162012-02-242012-02-21