即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法

摘要

ハードウェアには配線遅延があるためクロック周波数の向上に限界がある．そこで，実行時閥削減を目的としてクロックサイクルを消費しない即時通信がしばしば用いられる．そのような通信を行うサイクル精度動作記述には，組み合わせ回路としての閉路が発生することに起因する値の発振や発散の可能性といった難しさがある．そこで，本論文ではwireによる即時通信を行うサイクル精度動作記述モジュール群に発振や発散の問題が生じるか否か等を，モデル検査によって検証する手法を提案する．実験では上述した問題の発生を含hだ簡単なテストケース群に対して提案手法を適用し，その有効性を確認した．