スコアボードと局所的な不変条件を組み合わせる

検証の基準を入力の受け入れに置く

スコアボードは受け入れた各入力から期待結果を計算し、キューに入れます。出力の引き渡し時に最古の期待項目と比較します。各パイプラインレジスタを模倣せず契約から直接計算することで、共通のミスを減らします。入力ハンドシェイク時だけ追加してください。提示されても拒否された入力は未完了処理ではありません。

ADD入力tag10:(250,10)、tag11:(3,5)を受け入れたら、期待値は[(10,4,carry1),(11,8,carry0)]です。有効でもストールした出力では項目を取り出しません。tag10を引き渡したら、その項目だけ除きます。tag10の繰り返しや、値8にタグ12が付くのは、数値の一部が一致していても誤りです。関係するフラグと付随フィールドをすべて含めます。

局所的な不変条件は最終的な不一致だけでなく、最初に失敗したエッジを特定します。内部占有数はFIFO countと各段のvalidビットの和です。リセットやフラッシュを許す場合は取り消しの収支を追加し、両モニタに同じエッジ方針を使います。

数値境界とタイミングケースを組み合わせます。ゼロ、最大値、キャリーとボロー、連続通信、バブル、長いストール、満杯での置き換え、最終排出です。失敗を再現できるよう乱数シードを記録します。可能なら小さな制御空間を網羅します。

完了検査には進行の仮定とタイムアウトが必要です。受け取り側が以降ずっとreadyなら、未完了処理は排出されるはずです。永久ストールでは代わりに保持と占有数の上限を要求します。キャリーやタグ遅延を意図的に壊すと検査が失敗するべきです。この変異テストは感度を測ります。Nodeモデルの成功はHDL配線、X/Z動作、クロックドメイン交差、実装タイミングを検証しません。実際に観測した実行範囲だけを報告します。