マイクロプロセッサの形式的仕様記述・検証に関する研究

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

交付申請書に記載の通り、次の通り研究を行った。(1)形式的設計検証に関する研究従来の等価性や包含性の概念のもとでは、パイプライン処理などを行うマイクロプロセッサの等価性を論じることは難しかった。そこで、本研究では、レジスタやメモリなど命令セットによって仮定されている資源それぞれにおける値の変化に注目して、パイプラインやス-パスケーラなど種々の設計に対して、統一的な等価性の定義を与え、また、これに基づいた検証手法を開発した。また、この手法を実装するためには、大規模な回路の表現する関数に対する等価性判定など種々の演算を高速にまた少ない記憶容量で実現する必要性があることが明らかとなったため、二分モーメントグラフと呼ばれる、関数の新しい表現手法を導入して、特に従来手法では指数時間を要した乗算器に対する多項式時間の処理方式を新たに示した。これらの手法を融合させたマイクロプロセッサの検証システムの開発が今後の課題である。(2)仕様記述に関する研究これまで時相論理による仕様記述に対する検証手法の開発を行ってきており、この際、主に検証効率が良いことから分岐時間型の時相論理を用いてきたが、記述が直観に反し、繁雑であるといった問題点があった。これに対して、本研究では線形時間型の時相論理に基づく論理関数処理を用いた手法を開発・実装した。