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

1996 Fiscal Year Annual Research Report

• Project/Area Number: 08780276
• Research Institution: Osaka University
• Principal Investigator: 北道 淳司 大阪大学, 基礎工学部, 助手 (20234271)
• Keywords: 同期式順序回路 / 形式的検証 / 代数的手法 / シストリックアレイ / 高位設計 / 仕様記述 / 定理証明

Research Abstract

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

Research Products

• [Publications] 竹中崇: "シストリックアレーによる回路設計の正しさの一証明法" 情報処理学会第52回全国大会論文集. 6分冊. 3-4 (1996)
• [Publications] 竹中崇: "代数的手法によるPCIバスコントローラの設計検証" 情報処理学会研究報告. 97-DA-83. 9-16 (1997)
• [Publications] 斉藤義勝: "代数的手法を用いた複数の制御部を持つ同期式順序回路に対する設計および検証支援系の開発" 1997年春季電子情報通信学会全国大会論文集. (未発行).