| 講演名 | 2008-05-08 局所変数を含むアサーションに対するモデルチェッキングのためのチェッカ生成(アサーションベース検証,システム設計及び一般) 竹内 翔, 浜口 清治, 垣内 洋介, 柏原 敏伸, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 機能検証のための手段としてアサーションを用いたモデルチェッキングが注目されている.SVAでは,アサーション中に局所変数を用いることができるが,モデルチェッキングを考えた場合,局所変数の値を保存するための保存変数が一般に多数必要となり,計算量の点で問題となる.本稿では,モデルチェッキングに必要なメモリ量を削減することを目標に,保存変数の個数を各局所変数に対して1個に抑えるようなチェッカ生成アルゴリズムを提案する.提案アルゴリズムとLongとSeawrightによる先行研究との比較実験を行い,遅延回路やFIFO回路に対して検証時のメモリ使用量が10～30%改善されることを確認した. |
| 抄録(英) | To perform functional formal verification, model checking for assertions has been used. It is difficult, however, to handle assertions with local variables such as in System Verilog. The problem is that many storing variables for local variables are required, and having many storing variables increases the computational complexity of model checking. In this report, we show an algorithm for verification in order to reduce the number of storing variables. In particular, our algorithm requires only one storing variable for each local variable. We also show experimental results for our algorithm compared with the previous work by Long and Seawright, in which the memory requirement decreases by 10-30%. |
| キーワード(和) | モデルチェッキング / アサーション / 局所変数 / System Verilog |
| キーワード(英) | Model Checking / Assertion / Local Variable / System Verilog |
| 資料番号 | VLD2008-3 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2008/5/1(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 局所変数を含むアサーションに対するモデルチェッキングのためのチェッカ生成(アサーションベース検証,システム設計及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Checker Generation of Assertions with Local Variables for Model Checking |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデルチェッキング / Model Checking |
| キーワード(2)（和/英） | アサーション / Assertion |
| キーワード(3)（和/英） | 局所変数 / Local Variable |
| キーワード(4)（和/英） | System Verilog / System Verilog |
| 第 1 著者 氏名（和/英） | 竹内 翔 / Sho TAKEUCHI |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science & Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 浜口 清治 / Kiyoharu HAMAGUCHI |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science & Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 垣内 洋介 / Yosuke KAKIUCHI |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science & Technology, Osaka University |
| 第 4 著者 氏名（和/英） | 柏原 敏伸 / Toshinobu KASHIWABARA |
| 第 4 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science & Technology, Osaka University |
| 発表年月日 | 2008-05-08 |
| 資料番号 | VLD2008-3 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | 22 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |