| 講演名 | 2007/3/9 論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法(検証,組込技術とネットワークに関するワークショップETNET2007) 中村 一博, 成瀬 智啓, 高木 一義, 高木 直史, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では、SATを用いた論理回路の形式的検証の高速化を目指し、論理回路からSAT-solverの実行時間が短かくなるような和積標準形CNF論理式を生成する、CNF式生成処理フレームワークを提案する。提案するフレームワークは、回路分割と、部分回路のBDD生成、BDDからCNF式への変換から構成される。また本稿では、提案フレームワークに基づく、中間変数の間隔を考慮した回路分割、BDD生成、BDDからCNF式への変換アルゴリズムを示す。提案するCNF式生成手法と広く用いられているCNF式生成手法を実装し、SAT-solverの実行時間について比較を行ったところ、提案手法により実行時間が短縮されることが確認された。 |
| 抄録(英) | In this paper, we present a translation framework of circuits to CNF formulae for acceralating SAT-based formal verification. The translation framework consists of three elements, circuit partitioning, construction of BDDs and conversion of BDDs to CNF formulae. We also present a translation method of circuits to CNF formulae based on the translation framework. Experimental results show that the proposed method has effect on the reduction of SAT-solver execution time. |
| キーワード(和) | 充足可能性判定 / 二分決定グラフ / 和積標準形論理式 / 形式的検証 / 論理回路 |
| キーワード(英) | SAT / BDD / CNF formulae / formal verification / logic circuits |
| 資料番号 | CPSY2006-95,DC2006-109 |
| 発行日 |
| 研究会情報 | |
| 研究会 | DC |
|---|---|
| 開催期間 | 2007/3/9(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Dependable Computing (DC) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法(検証,組込技術とネットワークに関するワークショップETNET2007) |
| サブタイトル（和） | |
| タイトル（英） | Efficient Translation of Logic Circuits to CNF Formulae with BDD for Acceralating SAT-based Formal Verification |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 充足可能性判定 / SAT |
| キーワード(2)（和/英） | 二分決定グラフ / BDD |
| キーワード(3)（和/英） | 和積標準形論理式 / CNF formulae |
| キーワード(4)（和/英） | 形式的検証 / formal verification |
| キーワード(5)（和/英） | 論理回路 / logic circuits |
| 第 1 著者 氏名（和/英） | 中村 一博 / Kazuhiro NAKAMURA |
| 第 1 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 2 著者 氏名（和/英） | 成瀬 智啓 / Tomohiro NARUSE |
| 第 2 著者 所属（和/英） | 名古屋大学工学部 School of Engineering, Nagoya University |
| 第 3 著者 氏名（和/英） | 高木 一義 / Kazuyoshi TAKAGI |
| 第 3 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 4 著者 氏名（和/英） | 高木 直史 / Naofumi TAKAGI |
| 第 4 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 発表年月日 | 2007/3/9 |
| 資料番号 | CPSY2006-95,DC2006-109 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 604 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |