講演名 2020-11-17
Efficient computation of inductive invariant through flipflop selection
王 富東(東大), 藤田 昌宏(東大),
PDFダウンロードページ PDFダウンロードページへ
抄録(和)
抄録(英) As we all know, verification plays more and more important role in VLSI design and manufacture. However, it always takes too long time to affect efficiency and be costly. Inductive invariant which can represent the reachable states of circuits could be used to accelerate verification procedure. So main question we need to solve in this paper is how to generate inductive invariant efficiently. In general, we try to explore the dependency and coherence among all state variables which could be quantified by generating parameters and help us select flipflops instead of manually picking them up. The experiments on benchmark ISCA89 and ITC99 show effectiveness of the proposed method. Furthermore, the generated inductive invariant which represents exact or supersets of reachable states can be used to check if it intersects with bad states to prove circuit properties, which can be applied to various types of reachability-based analysis. The experimental results of reachability analysis on benchmark circuit HWMCC are also given.
キーワード(和)
キーワード(英) Inductive InvariantLarch affinityreachability AnalysisFlipflop Selection
資料番号 VLD2020-20,ICD2020-40,DC2020-40,RECONF2020-39
発行日 2020-11-10 (VLD, ICD, DC, RECONF)

研究会情報
研究会 VLD / DC / RECONF / ICD / IPSJ-SLDM
開催期間 2020/11/17(から2日開催)
開催地(和) オンライン開催
開催地(英) Online
テーマ(和) デザインガイア2020 -VLSI設計の新しい大地-
テーマ(英) Design Gaia 2020 -New Field of VLSI Design-
委員長氏名(和) 福田 大輔(富士通研) / 高橋 寛(愛媛大) / 柴田 裕一郎(長崎大) / 永田 真(神戸大) / 中村 祐一(NEC)
委員長氏名(英) Daisuke Fukuda(Fujitsu Labs.) / Hiroshi Takahashi(Ehime Univ.) / Yuichiro Shibata(Nagasaki Univ.) / Makoto Nagata(Kobe Univ.) / Yuichi Nakamura(NEC)
副委員長氏名(和) 小林 和淑(京都工繊大) / 土屋 達弘(阪大) / 佐野 健太郎(理研) / 山口 佳樹(筑波大) / 高橋 真史(キオクシア)
副委員長氏名(英) Kazutoshi Kobayashi(Kyoto Inst. of Tech.) / Tatsuhiro Tsuchiya(Osaka Univ.) / Kentaro Sano(RIKEN) / Yoshiki Yamaguchi(Tsukuba Univ.) / Masafumi Takahashi(masafumi2.takahashi@kioxia.com)
幹事氏名(和) 桜井 祐市(日立) / 兼本 大輔(大阪大学) / 新井 雅之(日大) / 難波 一輝(千葉大) / 三好 健文(イーツリーズ・ジャパン) / 小林 悠記(NEC) / 柘植 政利(ソシオネクスト) / 廣瀬 哲也(阪大) / 瀬戸 謙修(東京都市大) / 密山 幸男(高知工科大) / 君家 一紀(三菱電機) / 廣本 正之(富士通研)
幹事氏名(英) Yuichi Sakurai(Hitachi) / Daisuke Kanemoto(Osaka Univ.) / Masayuki Arai(Nihon Univ.) / Kazuteru Namba(Chiba Univ.) / Takefumi Miyoshi(e-trees.Japan) / Yuuki Kobayashi(NEC) / Masatoshi Tsuge(Socionext) / Tetsuya Hirose(Osaka Univ.) / Kenshu Seto(Tokyo City Univ.) / Yukio Mitsuyama(Kochi Univ. of Tech.) / Kazuki Oya(Mitsubishi Electric) / Masayuki Hiromoto(Fujistu Lab.)
幹事補佐氏名(和) 西元 琢真(日立) / / 中原 啓貴(東工大) / 竹村 幸尚(インテル) / 新居 浩二(TSMCデザインテクノロジージャパン) / 宮地 幸祐(信州大) / 久保木 猛(九大)
幹事補佐氏名(英) Takuma Nishimoto(Hitachi) / / Hiroki Nakahara(Tokyo Inst. of Tech.) / Yukitaka Takemura(INTEL) / Koji Nii(TSMC) / Kosuke Miyaji(Shinshu Univ.) / Takeshi Kuboki(Kyushu Univ.)

講演論文情報詳細
申込み研究会 Technical Committee on VLSI Design Technologies / Technical Committee on Dependable Computing / Technical Committee on Reconfigurable Systems / Technical Committee on Integrated Circuits and Devices / Special Interest Group on System and LSI Design Methodology
本文の言語 ENG
タイトル(和)
サブタイトル(和)
タイトル(英) Efficient computation of inductive invariant through flipflop selection
サブタイトル(和)
キーワード(1)(和/英) / Inductive InvariantLarch affinityreachability AnalysisFlipflop Selection
第 1 著者 氏名(和/英) 王 富東 / Fudong Wang
第 1 著者 所属(和/英) 東京大学(略称:東大)
University of Tokyo(略称:U-Tokyo)
第 2 著者 氏名(和/英) 藤田 昌宏 / Masahiro Fujita
第 2 著者 所属(和/英) 東京大学(略称:東大)
University of Tokyo(略称:U-Tokyo)
発表年月日 2020-11-17
資料番号 VLD2020-20,ICD2020-40,DC2020-40,RECONF2020-39
巻番号(vol) vol.120
号番号(no) VLD-234,ICD-235,DC-236,RECONF-237
ページ範囲 pp.54-59(VLD), pp.54-59(ICD), pp.54-59(DC), pp.54-59(RECONF),
ページ数 6
発行日 2020-11-10 (VLD, ICD, DC, RECONF)