WEKO3
アイテム
FSMへの変換に基づくHW/SW協調設計の形式的検証手法に関する研究
https://ipsj.ixsq.nii.ac.jp/records/27174
https://ipsj.ixsq.nii.ac.jp/records/27174e4b5c8fb-4d45-4685-a2fc-0b78822b26f9
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SLDM04119007.pdf (978.7 kB)
|
Copyright (c) 2005 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2005-03-17 | |||||||
| タイトル | ||||||||
| タイトル | FSMへの変換に基づくHW/SW協調設計の形式的検証手法に関する研究 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Formal Verification of HW/SW Co-design with FSM Translation | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 東京大学工学部電子工学科 | ||||||||
| 著者所属 | ||||||||
| 東京大学大学院工学系研究科電子工学専攻 | ||||||||
| 著者所属 | ||||||||
| 東京大学大規模集積システム設計教育研究センター | ||||||||
| 著者所属 | ||||||||
| 東京大学大規模集積システム設計教育研究センター | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Department of Electronics Engineering, Faculty of Engineering, University of Tokyo | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Department of Electronics Engineering, School of Engineering University of Tokyo | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| VLSI Design and Education Center, University of Tokyo | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| VLSI Design and Education Center, University of Tokyo | ||||||||
| 著者名 |
西原, 佑
× 西原, 佑
|
|||||||
| 著者名(英) |
Tasuku, NISHIHARA
× Tasuku, NISHIHARA
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本稿では，ハードウェアがVerilogやVHDLなどによりRTLで，ソフトウェアがC言語などによりプログラムコードで記述された，ハードウェア／ソフトウェア強調設計記述に対して形式的検証を適用する手法を提案する．提案する手法の特徴は，設計におけるハードウェアとソフトウェアの両記述を自動的に抽象化されたFSMへと変換し，既存のプロパティ検証器で一緒に検証を行う点である．本稿で扱う形式的検証は，プロパティ検証と，ハードウェア／ソフトウェア分割前のソフトウェア設計と分割後のハードウェア／ソフトウェア協調設計間の等価性検証である．両者について検証全体の流れと，幾つかの例題に対しての実験結果を示した。 | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | In this paper we present a methodology for formal verification of common hardware/software co-design. Two methodologies are proposed. 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11451459 | |||||||
| 書誌情報 |
情報処理学会研究報告システムLSI設計技術（SLDM） 巻 2005, 号 27(2004-SLDM-119), p. 37-42, 発行日 2005-03-17 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
