| 講演名 | 1999/1/11 HDLで記述されたハードウェア設計の時相論理による検証 櫟 粛之, 澤田 宏, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では, ハードウェア記述言語(HDL)で記述されたハードウェアの仕様を, その記述から直接, 形式的手法を用いて検証する方法を提案する.対象とするHDLは, ハードウェア合成システムPARTHENONで用いられるHDL(SFLと呼ばれる)である.この方法の核となる部分は, SFLで記述されたハードウェアの動作の記述を, その状態遷移関係を表現するブール式に自動変換することである.このブール式が, 時相論理CTLのよく知られたモデルチェックアルゴリズムにかけられ, CTL式で表現されたハードウェアの性質が検証される.本稿では, モデルチェックアルゴリズムの検証の結果がSFLの動作セマンティクスに正確に対応するためには, SFLの各動作をどのように論理表現すればよいかを示す. |
| 抄録(英) | In this paper, we introduce a method of formally verifying specifications on hardware directly from their descriptions in HDL (Hardware Description Language). The method is focused on SFL, the HDL of the hardware synthesis system PARTHENON. The essential part of the method is transformation of SFL descriptions to the Boolean formulas which represent the relation of state transition of the hardware. In this transformation, several devices are required to create the Boolean formula that behaves precisely in accordance with the semantics of SFL when it is applied to the standard backward model checking algorithm of temporal logic CTL. We discuss the problem in detail. |
| キーワード(和) | 形式的検証 / HDL / 時相論理 / 自動合成 / PARTHENON |
| キーワード(英) | formal verification / HDL / temporal logic / architecture synthesis / PARTHENON |
| 資料番号 | AI98-66 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 1999/1/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | HDLで記述されたハードウェア設計の時相論理による検証 |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification of Hardwere Described in HDL Using Temporal Logic |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式的検証 / formal verification |
| キーワード(2)（和/英） | HDL / HDL |
| キーワード(3)（和/英） | 時相論理 / temporal logic |
| キーワード(4)（和/英） | 自動合成 / architecture synthesis |
| キーワード(5)（和/英） | PARTHENON / PARTHENON |
| 第 1 著者 氏名（和/英） | 櫟 粛之 / Tadashi Araragi |
| 第 1 著者 所属（和/英） | NTTコミュニケーション科学研究所 NTT Communication Science Laboratories |
| 第 2 著者 氏名（和/英） | 澤田 宏 / Hiroshi Sawada |
| 第 2 著者 所属（和/英） | NTTコミュニケーション科学研究所 NTT Communication Science Laboratories |
| 発表年月日 | 1999/1/11 |
| 資料番号 | AI98-66 |
| 巻番号（vol） | vol.98 |
| 号番号（no） | 498 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |