論理関数処理による記号シミュレーションと無解釈評価に基づくプロセッサの形式的検証

点击翻译按钮获取中文摘要

本研究では形式的検証法をプロセッサに適用することを試みた.できる限り大規模なハードウェアに形式的検証法を適用するための計算手法の開発を目標に研究を進め,「記号シミュレーション」と「無解釈評価」を用いた方法に基づく処理系の試作とその評価を行なった.(1)アルゴリズムの検討現在までに得られているアイデアを具体化し,計算機上での処理に適した計算手順をまとめた.検証したいプロセッサの動作を,リファレンスプロセッサとよぶ単純なハードウェアで同じ命令セットを実行するプロセッサと比較する.この際に,複雑な算術演算は,同じ計算が行なわれたことだけを完全に検証することにより,計算量を大幅に削減した.(2)処理系の実現2つのプロセッサの動作の比較は,順序機械の記号モデル検査法のプログラムであるSMV(CMUで開発されたもの)を用いて行なった.「パイプラインALU」と呼ばれる小規模例題による実験と,DLXプロセッサに対して適用を行ない,3,000ゲートレベルのプロセッサまでなら30時間程度で検証が行なえる目処がついた.しかし,これ以上の規模のプロセッサに適用するには,さらに工夫が必要であることが判明した.(3)論理関数処理の新しいアルゴリズムの考案検証の時間とほとんどは,論理関数処理に費やされる.これまで,二分決定グラスを用いた手法が用いられてきたが,この方法ではメモリ要求が爆発的に増大する例が知られていた.本研究では,このような問題に対して,二分決定グラフのグラフ構造を非明治的に論理関数表現し,これを再び二分決定グラフで表すというデータ構造と,これに対するアルゴリズムを開発し,その評価を行なった.