| 研究概要 |
平成19年度は交付申請書の(1)および(2)に対応して以下の2項目について研究を行った.
(1)平成19年度に拡張したARITH記述に対する形式的検証手法を検討した.拡張したARITHでは,算術式と論理式が混在したハードウェアアルゴリズムを記述可能である.従来のARITH記述への形式的検証手法を拡張し,論理式から算術式への等価変換を行ったうえで数式処理により正当性を証明する手法について検討するとともに,プロトタイプソフトウェアを開発した.また,数式処理による検証手法のみでは算術演算を論理レベルで最適化したアルゴリズム等の場合に検証時間が増大すると予想されるため,並行して^*BMD(Multiplicative Binary Moment Diagram)に基づく従来の形式的検証技術をARITH記述に適用する手法を検討した.従来の検証手法と数式処理による検証手法を連携したプロトタイプ処理系のテストを行うとともに検証の実行時間や信頼性などの評価実験を実施した.
(2)平成19年度に設計したデータパスモジュールの性能評価を実施した.代表的なアルゴリズムに基づくモジュールを系統的に生成し,論理合成および配置配線ソフトウェアにより性能を概算した.性能評価の結果は,参照データとしてWeb上に公開した.また,拡張したARITHの応用として,暗号処理向けデータパスモジュールの自動生成を試みた.特に,RSAやElGamal暗号といった公開鍵暗号方式で必須となるモンゴメリ乗算器の生成をターゲットとした.モンゴメリ乗算器には多様な実現方法が存在するが,特に積和演算器を基本とした回路構造の生成を実施した.
|
