順序回路の上位設計記述における等価性指定の自動化手法

摘要

上位設計記述に対する等価性検証では、トランザクションごとに周期的な動作を繰り返す設計を検証する際に、レイテンシとスループットを用いて等価性を指定する手法やそれに基づく検証ツールが提案されている。しかし、その指定には、設計と指定法の両者についての知識が必要となる。本研究では、レイテンシとスループットによる等価性を自動的に推定する手法を提案する。提案手法では、ランダムシミュレーションの結果から入出力信号のレイテンシとスループットの値を絞り込む。加えて、より効率的な推定のために、タグシミュレーションによって、可能性のあるレイテンシとスループットを限定する手法も併せて提案する。いくつかの例題に対する実験において、タグシミュレーションによるレイテンシとスループットの範囲の絞込み、および、ランダムシミュレーションによる2つの設計間で成り立つ等価性の推定が行えることを示す。