| Research Abstract |
平成20年度は,(1)計算機代数を応用した形式的検証手法および(2)高信頼なデータパスジェネレータに関する研究を平行して実施し,それぞれ以下の成果を得た.
(1)大規模な算術演算回路に対する効率的な機能検証手法の実現を目指し,まず,重み数系と整数方程式を用いて算術演算回路を統一的に表現可能なデータ構造を提案した.このデータ構造に対する検証手法として,グレブナー基底や多項式簡約など計算機代数の手法に基づく手法を提案した.また,従来の形式的検証手法との比較し,算術演算回路の種類に応じて提案手法と従来手法を切り替えることで,検証時間を大幅に削減できることを明らかにした.
(2)提案手法に基づく検証系を組み込んだモジュールジェネレータを開発した.本システムは,多入力加算や積和演算などの多様な算術アルゴリズムをライブラリとして有し,その組み合わせで900種類を越える演算器モジュールを自動生成することができる.また,計算機代数に基づく形式的検証を適用することにより,64ビットの演算器であれば数分以内に検証することができる.本システムを公開したWebページ(http://www.aoki.ecei.tohoku.ac.jp/arith/mg/)は,平成20年度末までに12万件以上利用されている.
以上の研究により,計算機代数に基づく算術演算回路の形式的設計手法を提案し,その有効性を示すとともに,実用性の高い演算器モジュールジェネレータを実現した.
|
