シストリックアレイの形式的検証システムに関する研究

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

研究計画に従い行った研究の概要を述べる.(1)シストリックアレイの形式的記述法 本研究では,回路仕様記述において回路の大きさをパラメータ付で記述する仕様記述法を提案し,その記述のもとで任意の回路の大きさで,設計の正しさを形式的に定義した.この記述法のもとで,形式的回路検証法のベンチマーク問題の一つである行列の積などを求めるシストリックアレイ回路(Benchmark-Circuits for Hardware-Verification,TPCD94,Vol.901,LN in Computer Science,1995)に対する要求仕様及びその設計を行った.(2)シストリックアレイの形式的検証上記(1)で行った設計が正しいことの検証手順を提案し,実際にシステムを用いて検証を行った.検証は,回路の大きさによる帰納法を用いることによって設計されたシストリックアレイ回路が任意の大きさ(入出力データのサイズなど)で要求仕様を満足することを示すことである.帰納法を用いた検証においては,中間補題を考案すること,及び,その中間補題が与えられた実現仕様のもとで成立することを証明することなどの作業ステップからなる.作成するシステムは,要求仕様,実現仕様,中間補題などからの検証に必要な式の合成機能,その式が恒真であることを証明する定理証明系からなる.合成機能に関しては,必要な補題を設定,自動的な簡約・変形を行う.定理証明系としては,すでに我々の研究グループで開発したルーチン(試験研究05558031など)を利用して作成し,本手法の評価を行った.本設計法及び検証法に関しては,情報処理学会第52回全国大会にて,システムに関しては1997年春季電子情報通信学会全国大会にて成果発表を行った.