セキュリティハードウェアの形式的設計・検証理論の深化と展開

本年度は，ガロア体上の算術演算（ガロア体算術演算）のZDD（Zero-suppressed Decision Diagram）表現を用いた形式的検証手法の開発を推進した．特に，前年度から開発を推進してきた冗長表現と非冗長表現が混在するガロア体算術演算回路の形式的表現手法に対応する（機能検証の対象となる）HDL記述の等価性を判定する検証手法に関する理論を構築した．ここでは，提案する形式的表現による回路仕様と任意のHDL記述の等価性判定問題をいかに代数的問題（多項式イデアル所属問題）に帰着させるかが重要となる．そこで，開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式集合と見なして，その正規形であるグレブナー基底を導出した．ここで，特に，特殊な変数順序（逆トポロジー項順序）で多項式をZDDに変換することを見出した．この変数順序で変換されたZDD集合はグレブナー基底と等価なことを数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できるという特長を有する．その上で，その動作検証を目的として，簡易なガロア体演算回路（32ビットガロア体乗算器等）の仕様と回路記述から得られたZDD集合間の等価性判定を実行した．その結果から，考案手法により高速かつ完全な検証が可能となる見通しを得た．さらに，考案した形式的検証手法を定式化するとともに，そのプロトタイプソフトウェアを開発した．以上，当初計画していた形式的検証手法の見通しが得られた．

本年度は，ガロア体上の算術演算（ガロア体算術演算）のZDD（Zero-suppressed Decision Diagram）表現を用いた形式的検証手法の開発を推進した．特に，前年度から開発を推進してきた冗長表現と非冗長表現が混在するガロア体算術演算回路の形式的表現手法に対応する（機能検証の対象となる）HDL記述の等価性を判定する検証手法に関する理論を構築した．ここでは，提案する形式的表現による回路仕様と任意のHDL記述の等価性判定問題をいかに代数的問題（多項式イデアル所属問題）に帰着させるかが重要となる．そこで，開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式集合と見なして，その正規形であるグレブナー基底を導出した．ここで，特に，特殊な変数順序（逆トポロジー項順序）で多項式をZDDに変換することを見出した．この変数順序で変換されたZDD集合はグレブナー基底と等価なことを数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できるという特長を有する．その上で，その動作検証を目的として，簡易なガロア体演算回路（32ビットガロア体乗算器等）の仕様と回路記述から得られたZDD集合間の等価性判定を実行した．その結果から，考案手法により高速かつ完全な検証が可能となる見通しを得た．さらに，考案した形式的検証手法を定式化するとともに，そのプロトタイプソフトウェアを開発した．以上，当初計画していた形式的検証手法の見通しが得られた．