| 講演名 | 2004/3/4 C言語を対象とした記述間の差異に基づく効率的な等価性検証手法(システムオンシリコン設計技術並びにこれを活用したVLSI) 松本 剛史, 齋藤 寛, 藤田 昌宏, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では、C言語を対象とした記号シミュレーションによる効率的な等価性検証の手法を提案する。検証の対象は、ハードウェア化のために、原則としてポインタや再帰呼び出しを取り除いた、制限されたC言語プログラムとしている。検証は、与えられた2つのC言語記述に対する記号シミュレーションの結果を用いて行われる。従来の手法では、それぞれの記述の差異に対して等価性を判定して全体の等価性を導いていたが、等価でない差異がある場合は、それ以降の全ての文に対して等価性判定をする必要があり、非効率的であった。本稿では、記述間の差異を利用して検証が必要な関数に対してのみ記号シミュレーションを行い、また、記述が等しい部分のシミュレーションでは、等価性判定を省略することによって、差異の小さな2つの記述を効率的に検証できる手法を提案する。 |
| 抄録(英) | In this paper, an efficient equivalence cheking method for C descriptions is described. Since the descriptions to be verified are assumed to be HW implementation, they have some restrictions such as no pointer references, no recursive calls, and so on. The equivalence of two C descriptions is proved by using the result of symbolic simulation. In our previous method, the equivalence of two C descriptions was proved based on equivalence of variables in textual difference. However, this method was inefficient when there were inequivalent variables in the descriptions because all codes related to then might be verified the equivalence. In our new method, by verifying only functions that have textual difference and by omitting verification of codes that are textually equivalent, the efficiency is improved. |
| キーワード(和) | Cベース設計 / 等価性検証 / 記号シミュレーション |
| キーワード(英) | C-based Design / Equivalence Checking / Symbolic Simulation |
| 資料番号 | VLD2003-146 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2004/3/4(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | C言語を対象とした記述間の差異に基づく効率的な等価性検証手法(システムオンシリコン設計技術並びにこれを活用したVLSI) |
| サブタイトル（和） | |
| タイトル（英） | An Efficient Equivalence Checking Method for C Descriptions Based on Textual Differences |
| サブタイトル（和） | |
| キーワード(1)（和/英） | Cベース設計 / C-based Design |
| キーワード(2)（和/英） | 等価性検証 / Equivalence Checking |
| キーワード(3)（和/英） | 記号シミュレーション / Symbolic Simulation |
| 第 1 著者 氏名（和/英） | 松本 剛史 / Takeshi MATSUMOTO |
| 第 1 著者 所属（和/英） | 東京大学大学院工学系研究科電子工学専攻 Department of Electronic Engineering, University of Tokyo |
| 第 2 著者 氏名（和/英） | 齋藤 寛 / Hiroshi SAITO |
| 第 2 著者 所属（和/英） | 東京大学先端科学技術研究センター Research Center for Advances Science and Technology, University of Tokyo |
| 第 3 著者 氏名（和/英） | 藤田 昌宏 / Masahiro FUJITA |
| 第 3 著者 所属（和/英） | 東京大学大学院工学系研究科電子工学専攻 Department of Electronic Engineering, University of Tokyo |
| 発表年月日 | 2004/3/4 |
| 資料番号 | VLD2003-146 |
| 巻番号（vol） | vol.103 |
| 号番号（no） | 702 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |