WEKO3
アイテム
論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法
https://ipsj.ixsq.nii.ac.jp/records/33918
https://ipsj.ixsq.nii.ac.jp/records/339184d34ebca-26ec-4b74-9d1f-3ac8a1de8780
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-EMB07004019.pdf (586.6 kB)
|
Copyright (c) 2007 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2007-03-16 | |||||||
| タイトル | ||||||||
| タイトル | 論理回路のSATベース形式的検証の高速化のためのBDDを用いたCNF式生成手法 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Efficient Translation of Logic Circuits to CNF Formulae with BDD for Acceralating SAT-based Formal Verification | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学工学部 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学工学部 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| School of Engineering, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者名 |
中村, 一博
× 中村, 一博
|
|||||||
| 著者名(英) |
Kazuhiro, NAKAMURA
× Kazuhiro, NAKAMURA
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本稿では、SATを用いた論理回路の形式的検証の高速化を目指し、論理回路からSAT-solverの実行時間が短かくなるような和積標準形CNF論理式を生成する、CNF式生成処理フレームワークを提案する。提案するフレームワークは、回路分割と、部分回路のBDD生成、BDDからCNF式への変換から構成される。また本稿では、提案フレームワークに基づく、中間変数の間隔を考慮した回路分割、BDD生成、BDDからCNF式への変換アルゴリズムを示す。提案するＣＮＦ式生成手法と広く用いられているCNF式生成手法を実装し、SAT-solverの実行時間について比較を行ったところ、提案手法により実行時間が短縮されることが確認された。 | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA12149313 | |||||||
| 書誌情報 |
情報処理学会研究報告組込みシステム（EMB） 巻 2007, 号 27(2007-EMB-004), p. 107-112, 発行日 2007-03-16 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
