| Presentation | 2020-09-11 Inductive Invariant Generation Based on Binary Decision Diagram and its Application to Logic Synthesis Liu ZiHao, Miyasaka Yukio, Fujita Masahiro, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In this paper, we mainly focus on inductive invariant generation using binary decision diagram (BDD), and its application to the sequential circuit optimization. Inductive invariant is a function that satisfies the following condition: if the signals coming from flipflops are satisfied, then the signals going into those flipflops must be satisfied. In this research, we introduce two methods of generating the inductive invariant based on BDD, which are enlarging the onsets of the specific function and shrinking the onsets of the specific function. We show the extracted inductive invariants on ISCAS89, ITC99, and hwmcc07 benchmarks. Those inductive invariants can represent the supersets of reachable states so that we can utilize them for logic optimization as well as formal analysis. We show a simple experiment using the unreachable states as external don’t care to optimize the circuits. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Inductive invariantBinary decision Diagram |
| Paper # | RECONF2020-28 |
| Date of Issue | 2020-09-03 (RECONF) |
| Conference Information | |
| Committee | RECONF |
|---|---|
| Conference Date | 2020/9/10(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Online |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | Reconfigurable system, etc. |
| Chair | Yuichiro Shibata(Nagasaki Univ.) |
| Vice Chair | Kentaro Sano(RIKEN) / Yoshiki Yamaguchi(Tsukuba Univ.) |
| Secretary | Kentaro Sano(e-trees.Japan) / Yoshiki Yamaguchi(NEC) |
| Assistant | Hiroki Nakahara(Tokyo Inst. of Tech.) / Yukitaka Takemura(INTEL) |
| Paper Information | |
| Registration To | Technical Committee on Reconfigurable Systems |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Inductive Invariant Generation Based on Binary Decision Diagram and its Application to Logic Synthesis |
| Sub Title (in English) | |
| Keyword(1) | Inductive invariantBinary decision Diagram |
| 1st Author's Name | Liu ZiHao |
| 1st Author's Affiliation | University of Tokyo(UT) |
| 2nd Author's Name | Miyasaka Yukio |
| 2nd Author's Affiliation | University of Tokyo(UT) |
| 3rd Author's Name | Fujita Masahiro |
| 3rd Author's Affiliation | University of Tokyo(UT) |
| Date | 2020-09-11 |
| Paper # | RECONF2020-28 |
| Volume (vol) | vol.120 |
| Number (no) | RECONF-168 |
| Page | pp.pp.54-59(RECONF), |
| #Pages | 6 |
| Date of Issue | 2020-09-03 (RECONF) |