| Presentation | 2020-11-17 Efficient computation of inductive invariant through flipflop selection Fudong Wang, Masahiro Fujita, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Inductive InvariantLarch affinityreachability AnalysisFlipflop Selection |
| Paper # | VLD2020-20,ICD2020-40,DC2020-40,RECONF2020-39 |
| Date of Issue | 2020-11-10 (VLD, ICD, DC, RECONF) |
| Conference Information | |
| Committee | VLD / DC / RECONF / ICD / IPSJ-SLDM |
|---|---|
| Conference Date | 2020/11/17(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Online |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | Design Gaia 2020 -New Field of VLSI Design- |
| Chair | Daisuke Fukuda(Fujitsu Labs.) / Hiroshi Takahashi(Ehime Univ.) / Yuichiro Shibata(Nagasaki Univ.) / Makoto Nagata(Kobe Univ.) / Yuichi Nakamura(NEC) |
| Vice Chair | Kazutoshi Kobayashi(Kyoto Inst. of Tech.) / Tatsuhiro Tsuchiya(Osaka Univ.) / Kentaro Sano(RIKEN) / Yoshiki Yamaguchi(Tsukuba Univ.) / Masafumi Takahashi(masafumi2.takahashi@kioxia.com) |
| Secretary | Kazutoshi Kobayashi(Hitachi) / Tatsuhiro Tsuchiya(Osaka Univ.) / Kentaro Sano(Nihon Univ.) / Yoshiki Yamaguchi(Chiba Univ.) / Masafumi Takahashi(e-trees.Japan) / (NEC) |
| Assistant | Takuma Nishimoto(Hitachi) / / Hiroki Nakahara(Tokyo Inst. of Tech.) / Yukitaka Takemura(INTEL) / Koji Nii(TSMC) / Kosuke Miyaji(Shinshu Univ.) / Takeshi Kuboki(Kyushu Univ.) |
| Paper Information | |
| Registration To | 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 |
|---|---|
| Language | ENG |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Efficient computation of inductive invariant through flipflop selection |
| Sub Title (in English) | |
| Keyword(1) | Inductive InvariantLarch affinityreachability AnalysisFlipflop Selection |
| 1st Author's Name | Fudong Wang |
| 1st Author's Affiliation | University of Tokyo(U-Tokyo) |
| 2nd Author's Name | Masahiro Fujita |
| 2nd Author's Affiliation | University of Tokyo(U-Tokyo) |
| Date | 2020-11-17 |
| Paper # | VLD2020-20,ICD2020-40,DC2020-40,RECONF2020-39 |
| Volume (vol) | vol.120 |
| Number (no) | VLD-234,ICD-235,DC-236,RECONF-237 |
| Page | pp.pp.54-59(VLD), pp.54-59(ICD), pp.54-59(DC), pp.54-59(RECONF), |
| #Pages | 6 |
| Date of Issue | 2020-11-10 (VLD, ICD, DC, RECONF) |