2013 Fiscal Year Annual Research Report
ガロア体算術演算に基づくVLSIデータパスの形式的設計技術の開拓
| Project/Area Number |
25240006
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (A)
|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
本間 尚文 東北大学, 情報科学研究科, 准教授 (00343062)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
青木 孝文 東北大学, 情報科学研究科, 教授 (80241529)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | 計算機システム / システムオンチップ / VLSI設計技術 / 算術演算回路 / ガロア体 |
|---|
| Research Abstract |
平成25年度は，研究実施計画に基づいて下記2項目の研究を実施した．
1. 多項式基底表現されたガロア体算術演算回路の形式的表現手法の開発
ガロア体上の算術演算回路を形式的に表すグラフ表現「ガロア体算術回路グラフ(GF-ACG: Galois-Field Arithmetic Circuit Graph)」の理論を構築した．多項式基底表現されたガロア体は，整数環との代数的な類似性に着目すると，整数における各桁の“重み”がガロア体では“基底”に，各桁の“取り得る値”が多項式表現されたガロア体では“多項式係数の取り得る値”に対応する．これに加えて，整数では暗黙的に演算（加算や乗算）の規則が定義されていたが，ガロア体では既約多項式として演算規則を明示的に定義する必要がある．以上の観点から，基底の集合，多項式係数の取り得る値の集合，既約多項式によってガロア体を形式的に定義する手法を考案した．定義されるガロア体はプログラム言語におけるいわゆる変数の型に相当する．その変数を用いてGF-ACG を定式化した．
2. 多項式基底表現されたガロア体算術演算回路の形式的検証手法の開発
上記で開発するGF-ACG が表す回路機能の形式的検証手法の理論を構築した．その基本アイデアは，検証対象となる（ガロア体上の算術演算で表現される）回路機能の正当性を判定する問題を多項式イデアル所属問題に帰着させることである．開発手法では，まず，検証対象となる機能との等価性判定に用いる内部回路記述を多項式集合と見なしてグレブナー基底に変換する．この変換にはブッフバーガーアルゴリズムを用いた．次に，得られたグレブナー基底を用いて多項式簡約を実行することにより，検証対象の機能が多項式集合により導出できるかどうかを判定する．本研究では，以上の形式的検証手法を定式化するとともに，そのプロトタイプソフトウェアを開発した．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
当初の計画を上回り，正規基底表現されたガロア体上の算術演算回路への適用に関して一部先行して成果が得られている．
|
| Strategy for Future Research Activity |
現在は順調に開発・実験がなされており，引き続き研究計画に沿って推進する．
|
