| 講演名 | 2005/3/10 FSM への変換に基づく HW/SW 協調設計の形式的検証手法に関する研究(設計・合成, 組込技術とネットワークに関するワークショップ) 西原 佑, 松本 剛史, 小松 聡, 藤田 昌宏, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では, ハードウェアがVerilogやVHDLなどによりRTLで, ソフトウェアがC言語などによりプログラムコードで記述された, ハードウェア/ソフトウェア協調設計記述に対して形式的検証を適用する手法を提案する.提案する手法の特徴は, 設計におけるハードウェアとソフトウェアの両記述を自動的に抽象化されたFSMへと変換し, 既存のプロパティ検証器で一緒に検証を行う点である.本稿で扱う形式的検証は, プロパティ検証と, ハードウェア/ソフトウェア分割前のソフトウェア設計と分割後のハードウェア/ソフトウェア協調設計間の等価性検証である.両者について検証全体の流れと, 幾つかの例題に対しての実験結果を示した. |
| 抄録(英) | In this paper we present a methodology for formal verification of common hardware/software co-design. Two methodologies are proporsed. One is for property checking of hardware/software co-design in C/RTL, and the other is for equivalence checking between software design in C and hardware/software co-design in C/RTL converted from the software design. We extract caluculation part from them, abstract transactions between hardware and software, translate the description into finite state machines, and verify them with existing property checking tools. We report experimental results with a couple of examples. |
| キーワード(和) | ハードウェア/ソフトウェア協調検証 / 形式的検証 / C言語 |
| キーワード(英) | HW/SW Co-verification / Formal Verification / C / RTL / FSM |
| 資料番号 | CPSY2004-96 |
| 発行日 |
| 研究会情報 | |
| 研究会 | CPSY |
|---|---|
| 開催期間 | 2005/3/10(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Computer Systems (CPSY) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | FSM への変換に基づく HW/SW 協調設計の形式的検証手法に関する研究(設計・合成, 組込技術とネットワークに関するワークショップ) |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification of HW/SW Co-design with FSM Translation |
| サブタイトル（和） | |
| キーワード(1)（和/英） | ハードウェア/ソフトウェア協調検証 / HW/SW Co-verification |
| キーワード(2)（和/英） | 形式的検証 / Formal Verification |
| キーワード(3)（和/英） | C言語 / C |
| 第 1 著者 氏名（和/英） | 西原 佑 / Tasuku NISHIHARA |
| 第 1 著者 所属（和/英） | 東京大学工学部電子工学科 Department of Electronics Engineering, Faculty of Engineering, University of Tokyo |
| 第 2 著者 氏名（和/英） | 松本 剛史 / Takeshi MATSUMOTO |
| 第 2 著者 所属（和/英） | 東京大学大学院工学系研究科 Department of Electronics Engineering, School of Engineering University of Tokyo |
| 第 3 著者 氏名（和/英） | 小松 聡 / Satoshi KOMATSU |
| 第 3 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター VLSI Design and Education Center, University of Tokyo |
| 第 4 著者 氏名（和/英） | 藤田 昌宏 / Masahiro FUJITA |
| 第 4 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター VLSI Design and Education Center, University of Tokyo |
| 発表年月日 | 2005/3/10 |
| 資料番号 | CPSY2004-96 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 737 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |