| Presentation | 2012/2/24 A consideration of logical circuit debugging method using unsatisfiability JAESUNG LEE, TAKESHI MATSUMOTO, MASAHIRO FUJITA, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Detecting errorneous behaviors in logic circuits and debugging are timeconsuming 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | |
| Paper # | Vol.2012-SLDM-155 No.5,Vol.2012-EMB-24 No.5 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2012/2/24(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Dependable Computing (DC) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A consideration of logical circuit debugging method using unsatisfiability |
| Sub Title (in English) | |
| Keyword(1) | |
| 1st Author's Name | JAESUNG LEE |
| 1st Author's Affiliation | Department of Electrical Engineering and Information Systems, School of Engineering, The University of Tokyo() |
| 2nd Author's Name | TAKESHI MATSUMOTO |
| 2nd Author's Affiliation | VLSI Design and Education Center, The University of Tokyo |
| 3rd Author's Name | MASAHIRO FUJITA |
| 3rd Author's Affiliation | VLSI Design and Education Center, The University of Tokyo:CREST, Japan Science and Technology Agency |
| Date | 2012/2/24 |
| Paper # | Vol.2012-SLDM-155 No.5,Vol.2012-EMB-24 No.5 |
| Volume (vol) | vol.111 |
| Number (no) | 462 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |