| 講演名 | 2005-01-25 分割統治法による形式的機能検証のためのインタフェイスプロトコルに対するアサーションの分割(設計・検証, FRGAとその応用及び一般) 松島 広直, 北嶋 暁, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では, ディジタルシステム設計のRT(Register Transfer)レベルにおいて, BCA(Bus Cycle Accurate)レベルでのインタフェースプロトコルに対するアサーション群をコンポーネント単位のアサーション群に分割し, それを用いて各コンポーネントの形式的な機能検証を行う方法を提案する.本手法により, 段階的設計における検証をコンポーネント単位の分割統治法により行うための, 各コンポーネントに対するインタフェイスプロトコルの制約が得られる.提案手法では, コンポーネントの入出力関係に着目し, アサーション群を分割する.例題について本手法を適用し, コンポーネント単位でのインタフェイスプロトコルの制約に対して, 満たすべき性質が検証可能であることが確認できた. |
| 抄録(英) | In this paper, a dividing technique of assertions for an interface protocol in a digital system is proposed for divide and conquer approach of formal verification. In the proposed technique, assertions in the description at the bus cycle accurate level of a system are divided into the assertions that are used in the descriptions of components at RT-level for each component. Input-output relation among components in the system is considered for the division. All components in a sample producer-consumer system was verified with assertions divided by the proposed technique. |
| キーワード(和) | 形式的検証 / アサーション / インタフェイスプロトコル / バスサイクルアキュレートレベル / 分割統治法 |
| キーワード(英) | formal verification / assertion / interface protocol / bus cycle accurate level / divide and conquer approach |
| 資料番号 | VLD2004-104,CPSY2004-70 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2005/1/18(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 分割統治法による形式的機能検証のためのインタフェイスプロトコルに対するアサーションの分割(設計・検証, FRGAとその応用及び一般) |
| サブタイトル（和） | |
| タイトル（英） | A Dividing Technique of Assertions for an Interface Protocol used in a Divide and Conquer Approach of Formal Verification |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式的検証 / formal verification |
| キーワード(2)（和/英） | アサーション / assertion |
| キーワード(3)（和/英） | インタフェイスプロトコル / interface protocol |
| キーワード(4)（和/英） | バスサイクルアキュレートレベル / bus cycle accurate level |
| キーワード(5)（和/英） | 分割統治法 / divide and conquer approach |
| 第 1 著者 氏名（和/英） | 松島 広直 / Hironao MATSUSHIMA |
| 第 1 著者 所属（和/英） | 大阪電気通信大学大学院工学研究科 Division of Information and Computer Sciences, Graduate School of Engineering, Osaka Electro-Communication University |
| 第 2 著者 氏名（和/英） | 北嶋 暁 / Akira KITAJIMA |
| 第 2 著者 所属（和/英） | 大阪電気通信大学大学院工学研究科 Division of Information and Computer Sciences, Graduate School of Engineering, Osaka Electro-Communication University |
| 発表年月日 | 2005-01-25 |
| 資料番号 | VLD2004-104,CPSY2004-70 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 589 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |