| 講演名 | 2020-09-11 ２分決定グラフを用いたInductive Invariantの計算手法とその論理合成への応用 劉 子豪(東大), 宮坂 幸雄(東大), 藤田 昌宏(東大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | |
| 抄録(英) | 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. |
| キーワード(和) | |
| キーワード(英) | Inductive invariantBinary decision Diagram |
| 資料番号 | RECONF2020-28 |
| 発行日 | 2020-09-03 (RECONF) |
| 研究会情報 | |
| 研究会 | RECONF |
|---|---|
| 開催期間 | 2020/9/10(から2日開催) |
| 開催地（和） | オンライン開催 |
| 開催地（英） | Online |
| テーマ（和） | リコンフィギャラブルシステム，一般 |
| テーマ（英） | Reconfigurable system, etc. |
| 委員長氏名（和） | 柴田 裕一郎(長崎大) |
| 委員長氏名（英） | Yuichiro Shibata(Nagasaki Univ.) |
| 副委員長氏名（和） | 佐野 健太郎(理研) / 山口 佳樹(筑波大) |
| 副委員長氏名（英） | Kentaro Sano(RIKEN) / Yoshiki Yamaguchi(Tsukuba Univ.) |
| 幹事氏名（和） | 三好 健文(イーツリーズ・ジャパン) / 小林 悠記(NEC) |
| 幹事氏名（英） | Takefumi Miyoshi(e-trees.Japan) / Yuuki Kobayashi(NEC) |
| 幹事補佐氏名（和） | 中原 啓貴(東工大) / 竹村 幸尚(インテル) |
| 幹事補佐氏名（英） | Hiroki Nakahara(Tokyo Inst. of Tech.) / Yukitaka Takemura(INTEL) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Reconfigurable Systems |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | ２分決定グラフを用いたInductive Invariantの計算手法とその論理合成への応用 |
| サブタイトル（和） | |
| タイトル（英） | Inductive Invariant Generation Based on Binary Decision Diagram and its Application to Logic Synthesis |
| サブタイトル（和） | |
| キーワード(1)（和/英） | / Inductive invariantBinary decision Diagram |
| 第 1 著者 氏名（和/英） | 劉 子豪 / Liu ZiHao |
| 第 1 著者 所属（和/英） | 東京大学(略称：東大) University of Tokyo(略称：UT) |
| 第 2 著者 氏名（和/英） | 宮坂 幸雄 / Miyasaka Yukio |
| 第 2 著者 所属（和/英） | 東京大学(略称：東大) University of Tokyo(略称：UT) |
| 第 3 著者 氏名（和/英） | 藤田 昌宏 / Fujita Masahiro |
| 第 3 著者 所属（和/英） | 東京大学(略称：東大) University of Tokyo(略称：UT) |
| 発表年月日 | 2020-09-11 |
| 資料番号 | RECONF2020-28 |
| 巻番号（vol） | vol.120 |
| 号番号（no） | RECONF-168 |
| ページ範囲 | pp.54-59(RECONF), |
| ページ数 | 6 |
| 発行日 | 2020-09-03 (RECONF) |