シミュレーションを利用した形式的検証システム

森広 芳文  米田 友洋  

誌名
電子情報通信学会論文誌 D   Vol.J84-D1   No.4   pp.367-377
発行日: 2001/04/01
Online ISSN: 
DOI: 
Print ISSN: 0915-1915
論文種別: 論文
専門分野: フォールトトレランス
キーワード: 
形式的検証,  シミュレーション,  状態遷移図,  同期式回路,  

本文: PDF(841.2KB)>>
論文を購入




あらまし: 
近年,検証を形式的に行おうという研究が活発に行われているが,実用レベルのシステムにそのまま適用するのは,必要メモリ量,及び仕様の形式的表現の難しさ等から現在のところ難しい.そこで本研究では,状態遷移図で表現される仕様から遷移関係を抽出し,シミュレーションを用いて回路を検証する方式について検討する.この方式では,抽出した遷移関係についてシミュレーションを行い,その結果を用いて回路の新たな遷移関係を作成している.これにより,検証アルゴリズムが終了した場合は,任意の入力系列について回路が仕様を満たしていることが保証され,また,検証アルゴリズムをk回目のループで中断した場合でも,任意の長さk以下の入力系列について回路が仕様を満たしてることが保証される.本方式を実装し,SCIのCache-controler,及び,Texas97 benchmark回路中のいくつかのモジュールについて検証を行った.