| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2008-03-28 08:45 準形式的モデル検査のハードウェア実装による高速化の検討 ○森下賢志・吉田浩章・藤田昌宏（東大）  DC2007-103 CPSY2007-99 |
|
| 抄録 | （和） | 近年設計が大規模になり、複雑化が進むにつれて検証の重要性が増している。現在の重要な検証手法の一つであるモデル検査には適用する回路規模が大きくなると状態爆発を起こし、実用的な時間内で検査が終了しないという問題がある。そのため回路規模や検証時間の面でより効率的なモデル検査が必要とされている。現在の効率的なモデル検査手法の1つに、コンパイルドシミュレーションを基にした準形式的限定モデル検査がある。本稿ではそのアルゴリズムの一部をハードウェアで実装し、各々の処理に対してハードウェア・ソフトウェア協調実行に向けた最適化を行うことで高速化したモデル検査を提案する。また例題を用いた実験によって実際に高速に検証を行い、提案手法の有効性を確認した。 |
| （英） | The verification becomes important now as the design becomes complex and large-scale.Model checking which is one of the most important verification has been held back by the state explosion problem, which is the problem that the number of states grows exponentially in the number of system components.So we propose an efficient model checking method in this paper.We have enhanced a semi-formal bounded model checking by using a hardware accelerator and modified the codes to be easily implemented on a hardware.The experimental results with some examples show that the proposed method can execute model checking in short time. | |
| キーワード | （和） | モデル検査 / / / / / / / |
| （英） | Model Checking / / / / / / / | |
| 文献情報 | 信学技報, vol. 107, no. 559, DC2007-103, pp. 115-120, 2008年3月. | |
| 資料番号 | DC2007-103 | |
| 発行日 | 2008-03-20 (DC, CPSY) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | DC2007-103 CPSY2007-99 |
|
| 研究会情報 | |
| 研究会 | DC CPSY IPSJ-SLDM IPSJ-EMB |
| 開催期間 | 2008-03-27 - 2008-03-28 |
| 開催地（和） | 屋久島 離島総合開発センター |
| 開催地（英） | |
| テーマ（和） | 組込技術とネットワークに関するワークショップ ETNET2008（コンピュータシステム研究会、情報処理学会システムLSI設計技術研究会、情報処理学会組込みシステム研究会共催） |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | DC |
| 会議コード | 2008-03-DC |
| 本文の言語 | 日本語 |
| タイトル（和） | 準形式的モデル検査のハードウェア実装による高速化の検討 |
| サブタイトル（和） | |
| タイトル（英） | A Hardware Acceleration for Semi-Formal Model Checking |
| サブタイトル（英） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | / |
| キーワード(3)（和/英） | / |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 森下 賢志 / Satoshi Morishita / モリシタ サトシ |
| 第1著者 所属（和/英） | 東京大学 (略称： 東大) University of Tokyo (略称： Univ of Tokyo) |
| 第2著者 氏名（和/英/ヨミ） | 吉田 浩章 / Hiroaki Yoshida / ヨシダ ヒロアキ |
| 第2著者 所属（和/英） | 東京大学 (略称： 東大) University of Tokyo (略称： Univ of Tokyo) |
| 第3著者 氏名（和/英/ヨミ） | 藤田 昌宏 / Masahiro Fujita / フジタ マサヒロ |
| 第3著者 所属（和/英） | 東京大学 (略称： 東大) University of Tokyo (略称： Univ of Tokyo) |
| 第4著者 氏名（和/英/ヨミ） | / / |
| 第4著者 所属（和/英） | (略称： ) (略称： ) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2008-03-28 08:45:00 |
| 発表時間 | 20分 |
| 申込先研究会 | DC |
| 資料番号 | DC2007-103, CPSY2007-99 |
| 巻番号（vol） | vol.107 |
| 号番号（no） | no.559(DC), no.558(CPSY) |
| ページ範囲 | pp.115-120 |
| ページ数 | 6 |
| 発行日 | 2008-03-20 (DC, CPSY) |
[研究会発表申込システムのトップページに戻る]