| 講演名 | 2006-11-28 動的局所変数を含むアサーションに対する限定モデルチェッキング(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会) 竹内 翔, 浜口 清治, 柏原 敏伸, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 回路をフォーマルに検証する手法として,アサーションに対する限定モデルチェッキングが注目されている.しかしながら,System Verilogに見られるような動的局所変数を含んだアサーションは計算量の点で扱いが困難である.そこで,本稿では動的局所変数を含むアサーションに対する限定モデルチェッキングについて主として必要メモリ量を削減するためのアルゴリズムを検討する.アルゴリズムを実装して実験した結果も示す. |
| 抄録(英) | To perform functional formal verification, bounded model checking for assertions has been proposed. For bounded model checking, however, it is difficult to handle assertions including dynamic local variables such as in System Verilog. In this report, we investigate an algorithm for verifying assertions including dynamic local variables with bounded model checking. This algorithm focuses on reduction in memory requirement. We implemented the algorithm and performed some experiments. |
| キーワード(和) | アサーションベース検証 / 限定モデルチェッキング / 動的局所変数 / System Verilog |
| キーワード(英) | Assertion-Based Verification / Bounded Model Checking / Dynamic Local Variable / System Verilog |
| 資料番号 | VLD2006-53,DC2006-40 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2006/11/21(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 動的局所変数を含むアサーションに対する限定モデルチェッキング(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会) |
| サブタイトル（和） | |
| タイトル（英） | Bounded Model Checking for Assertions including Dynamic Local Variables |
| サブタイトル（和） | |
| キーワード(1)（和/英） | アサーションベース検証 / Assertion-Based Verification |
| キーワード(2)（和/英） | 限定モデルチェッキング / Bounded Model Checking |
| キーワード(3)（和/英） | 動的局所変数 / Dynamic Local Variable |
| キーワード(4)（和/英） | System Verilog / System Verilog |
| 第 1 著者 氏名（和/英） | 竹内 翔 / Sho TAKEUCHI |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 浜口 清治 / Kiyoharu HAMAGUCHI |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 柏原 敏伸 / Tosinobu KASHIWABARA |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2006-11-28 |
| 資料番号 | VLD2006-53,DC2006-40 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 387 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |