| 研究課題/領域番号 |
17500047
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機システム・ネットワーク
|
|---|
| 研究機関 | 早稲田大学 |
|---|
研究代表者 |
木村 晋二 早稲田大学, 情報生産システム研究科, 教授 (20183303)
|
|---|
| 研究期間 (年度) |
2005 – 2007
|
| 研究課題ステータス |
完了 (2007年度)
|
| 配分額 *注記 |
3,630千円 (直接経費: 3,300千円、間接経費: 330千円)
2007年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2006年度: 1,000千円 (直接経費: 1,000千円)
2005年度: 1,200千円 (直接経費: 1,200千円)
|
|---|
| キーワード | 等価論理 / ハードウェアの等価検証 / 無評価関数 / 項書き換え / 高位検証 |
|---|
| 研究概要 |
ハードウェアの高位レベルの等価検証手法の確立を目的とし、類似度を考慮した等価論理に基づく等価検証システムの研究を行った。等価論理は、変数の等価性のみに着目した論理体系で、他の論理との組合せで高い検証機能を持つことが知られている。まず、Verilog記述から等価論理の式を生成するシステムと、C言語記述から等価論理の式を生成するシステム、およびこれらの変換された等価論理式を時間展開するシステムのプロトタイプの構築を行った。生成された時間展開後の等価論理式に対し、公開されている等価論理判定システムであるCVCLやYICESを適用し、本手法の正当性と有効性の確認を行った。また現状の等価論理判定手法が時間展開に対して指数的な計算量を必要とすることが実験的に確認できたため、等価論理式をSATの問題に帰着して解く手法について研究を行い、変数間の等価性の推移的閉方を効率化する手法の検討を行った。類似度については、等価論理式の枠内での導入を行い、絶対値の差に基づく手法、現在の変数値との差に基づく手法の検討を行った。またハードウェア設計における浮動小数点数の固定小数点数への変換時の誤差と類似度の関係についても研究を行い、固定小数点数のビット数の最適化手法を提案した。さらに具体的なハードウェアへの適用として、マルチスレッディングプロセッサの等価性検証、加算のプレフィックスグラフの最適化と等価性検証、プロトタイピングを用いた等価検証の高速化とプロトタイピング検証におけるアサーション検証手法の高速化について研究を行った。
|
