| 講演名 | 1999/6/11 高位設計における形式的検証のための整数上の制約論理式の真偽判定プログラムに対する改良手法 景山 洋行, 北道 淳司, 東野 輝夫, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 我々は論理回路の高位設計における形式的検証を行うために,整数変数及び整数演算を含むある制約論理のためのデータ構造を提案し,それに対する処理系を開発している.本論文では,提案するデータ構造及び処理系に対する,計算時間及び使用メモリサイズの改善法を提案し,それらを従来の処理系に組み込み,いくつかの検証例題を用いて評価実験を行った結果について述べる.提案しているデータ構造は,BDD (Binary Decision Diagram)を拡張したものであり,BDDの処理において知られている変数の順序付けや限定子の処理に対する高速化などの改良手法を提案する. |
| 抄録(英) | We have been studying the high level verification of logic circuits. In the verification at high level, we use Presburger arithmetic, which includes integer variables and some operators for them. We proposed a new data structure for Presburger arithmetic and implemented a library for them. In this paper, we propose some improvements on algorithms for our data structure. We refined our library and describe the restults of some experiments of formal design verification using our methods. Our data structure is like BDDs (Binary Decision Diagramas). Out improvements include the variable ordering for BDDs, the refinement of the operation for existential quantifier and so on. |
| キーワード(和) | 高位設計 / 形式的検証 / プレスブルガー文 / 二分決定グラフ |
| キーワード(英) | High Level Design / Formal Verification / Presburger Sentence / Binary Decision Diagrams |
| 資料番号 | CAS99-30 |
| 発行日 |
| 研究会情報 | |
| 研究会 | CAS |
|---|---|
| 開催期間 | 1999/6/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Circuits and Systems (CAS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 高位設計における形式的検証のための整数上の制約論理式の真偽判定プログラムに対する改良手法 |
| サブタイトル（和） | |
| タイトル（英） | Improvements of Decision Algorithm for Presburger Arithmetic in High Level Verification of Logic Circuits |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 高位設計 / High Level Design |
| キーワード(2)（和/英） | 形式的検証 / Formal Verification |
| キーワード(3)（和/英） | プレスブルガー文 / Presburger Sentence |
| キーワード(4)（和/英） | 二分決定グラフ / Binary Decision Diagrams |
| 第 1 著者 氏名（和/英） | 景山 洋行 / Hiroyuki KAGEYAMA |
| 第 1 著者 所属（和/英） | 大阪大学大学院基礎工学研究科 Graduate School of Engineering Science, Osaka University |
| 第 2 著者 氏名（和/英） | 北道 淳司 / Junji KITAMICHI |
| 第 2 著者 所属（和/英） | 大阪大学情報処理教育センター Education Center for Information Processing, Osaka University |
| 第 3 著者 氏名（和/英） | 東野 輝夫 / Teruo HIGASHINO |
| 第 3 著者 所属（和/英） | 大阪大学大学院基礎工学研究科 Graduate School of Engineering Science, Osaka University |
| 発表年月日 | 1999/6/11 |
| 資料番号 | CAS99-30 |
| 巻番号（vol） | vol.99 |
| 号番号（no） | 105 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |