| 講演名 | 2006-11-28 同値制約を考慮した第一階述語論理の決定可能なサブクラスによる等価性判定(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会) 小澤 弘明, 浜口 清治, 柏原 敏伸, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 大規模デジタル回路の形式的検証に対して、限量子を含まない等号付第一階述語論理の充足可能性判定を用いた手法が提案されている.しかしながら,この論理は加算における交換則のような特定の関数及び述語の性質を考慮しない.この問題に対処する一手段として,我々は関数及び述語の性質を表す式の集合である「同値制約」を導入する.本稿では,この制約の下で式の充足可能性を判定するアルゴリズムを提示し,実装,実験した結果を示す. |
| 抄録(英) | For formal verification of large-scale digital circuits, a method using satisfiability checking of logic with equality and uninterpreted functions has been proposed. This logic, however, does not consider specific properties of functions or predicates at all, e.g. commutative property of addition. In order to ease this problem, we introduce "equivalence constraint" that is a set of formulas representing the properties of functions and predicates. In this report, we show an algorithm for checking the satisfiability of formulas under the constraints and also show experimental results. |
| キーワード(和) | 等価性判定 / 限量子を含まない等号付第一階述語論理 / 同値制約 |
| キーワード(英) | equivalence check / logic with equality and uninterpreted functions / equivalence constraints |
| 資料番号 | VLD2006-52,DC2006-39 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2006/11/21(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 同値制約を考慮した第一階述語論理の決定可能なサブクラスによる等価性判定(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会) |
| サブタイトル（和） | |
| タイトル（英） | Equivalence Checking using a Decidable Subclass of First-Order-Logic under Equivalence Constraints |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 等価性判定 / equivalence check |
| キーワード(2)（和/英） | 限量子を含まない等号付第一階述語論理 / logic with equality and uninterpreted functions |
| キーワード(3)（和/英） | 同値制約 / equivalence constraints |
| 第 1 著者 氏名（和/英） | 小澤 弘明 / Hiroaki KOZAWA |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Infomation Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 浜口 清治 / Kiyoharu HAMAGUCHI |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Infomation Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 柏原 敏伸 / Toshinobu KASHIWABARA |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Infomation Science and Technology, Osaka University |
| 発表年月日 | 2006-11-28 |
| 資料番号 | VLD2006-52,DC2006-39 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 387 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |