| 講演名 | 2005/3/3 システムレベル設計における同期検証フレームワークの提案(高位設計-1, システムオンシリコン設計技術並びにこれを活用した VLSI) サクンコンチャック タンヤパット, 小松 聡, 藤田 昌宏, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | |
| 抄録(英) | This paper presents a formal verification framework targeting the synchronization problem in SpecC language, a C-based system-level design language that supports HW/SW design seamlessly. Based on the Counter-Example Guided Abstraction Refinement (CEGAR) paradigm, we can briefly describe our framework as follows. The SpecC descriptions are abstracted and translated into descriptions that contain only boolean variables, or so called "boolean SpecC". The boolean SpecC descriptions are translated into an equality/inequality formula. This formula is then checked using an Integer Linear Programming (ILP) solver. Once the results are satisfied, the verification process stops with the synchronization property holds. Otherwise, a counterexample is given. The process of counterexample analysis and abstraction refinement is also proposed in this paper. |
| キーワード(和) | |
| キーワード(英) | formal verification / model checking / predicate abstraction / abstraction refinement / synchronization verification |
| 資料番号 | VLD2004-136,ICD2004-232 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2005/3/3(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | システムレベル設計における同期検証フレームワークの提案(高位設計-1, システムオンシリコン設計技術並びにこれを活用した VLSI) |
| サブタイトル（和） | |
| タイトル（英） | A Framework on Synchronization Verification in System-Level Design |
| サブタイトル（和） | |
| キーワード(1)（和/英） | / formal verification |
| 第 1 著者 氏名（和/英） | サクンコンチャック タンヤパット / Thanyapat SAKUNKONCHAK |
| 第 1 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター |
| 第 2 著者 氏名（和/英） | 小松 聡 / Satoshi KOMATSU |
| 第 2 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター |
| 第 3 著者 氏名（和/英） | 藤田 昌宏 / Masahiro FUJITA |
| 第 3 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター |
| 発表年月日 | 2005/3/3 |
| 資料番号 | VLD2004-136,ICD2004-232 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 708 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |