講演名 2002/4/12
非同期式回路検証のためのレベル指向モデルとその効率的解析法について
小黒 裕介, 米田 友洋,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 非同期式回路のモデル化をレベル指向モデルを用いて行うことにより,モデル構築の容易化,可読性の向上,データパスの自然なモデル化という利点がある.一方,このようなレベル指向モデルの解析にも,従来の遷移指向モデルと同様に効率的解析手法の導入が必須である.そこで本稿では,あるレベル指向モデルを定義し,効率的解析手法の一つであるpartial order reductionをそれに適用するための技術について議論する.
抄録(英) Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for a little larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines one level oriented formal model based on time Petri nets, and then proposes its partial order reduction algorithm that prunes unnecessary state generation with guaranteeing the correctness of the verification.
キーワード(和) レベル指向モデル / 非同期式回路 / 形式的検証 / タイムペトリネット.
キーワード(英) Level oriented model / asynchronous circuits / formal verification / time Petri nets.
資料番号 DC2002-7
発行日

研究会情報
研究会 DC
開催期間 2002/4/12(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Dependable Computing (DC)
本文の言語 JPN
タイトル(和) 非同期式回路検証のためのレベル指向モデルとその効率的解析法について
サブタイトル(和)
タイトル(英) Level Oriented Formal Model for Asynchronous Circuit Verification and its Efficient Analysis Method
サブタイトル(和)
キーワード(1)(和/英) レベル指向モデル / Level oriented model
キーワード(2)(和/英) 非同期式回路 / asynchronous circuits
キーワード(3)(和/英) 形式的検証 / formal verification
キーワード(4)(和/英) タイムペトリネット. / time Petri nets.
第 1 著者 氏名(和/英) 小黒 裕介 / Yusuke OGURO
第 1 著者 所属(和/英) 東京工業大学大学院情報理工学研究科
Graduate School of Information Science and Engineering, Tokyo Institute of Technology
第 2 著者 氏名(和/英) 米田 友洋 / Tomohiro YONEDA
第 2 著者 所属(和/英) 東京工業大学大学院情報理工学研究科
Graduate School of Information Science and Engineering, Tokyo Institute of Technology
発表年月日 2002/4/12
資料番号 DC2002-7
巻番号(vol) vol.102
号番号(no) 28
ページ範囲 pp.-
ページ数 6
発行日