「形式的手法を用いた実用検証システム」 : 汎用機、スーパーコン、EWSの回路検証に全面適用

概要

論文の詳細を見る
汎用計算機等の装置は年々その規模、複雑さが増大し、装置の検証も非常に時間のかかるものとなってきている。これら大規模装置の設計の検証は、装置レベルで実際の試験診断プログラムを論理シミュレーションするのが普通である。しかし、装置レベルシミュレーションをゲートレベルで行うのは膨大な検証時間とマシンリソースが必要である。そこで、我々はRTレベルの装置レベルハードウェアシミュレータHAL IIIを用い、検証の主体をRTレベルの機能シミュレーションに置いている。ゲートレベルでのシミュレーションは行わず、ゲート回路の正当性は、RT記述との論理的な等価性を形式的検証で保証することによって行っている。本稿では当社の汎用機、スーパーコン、EWS等の設計検証に用いている形式的検証エンジンCONDORとこれを含んだ統合的論理検証システムEVERY7を用いた検証運用フローと検証例について示す。また、順序回路検証を実回路に適用した実験事例についても紹介する。
社団法人電子情報通信学会の論文
1995-09-05