検証計画・カバレッジ・独立した参照モデル

検証計画は仕様を検査可能な主張へ変えます

「正しく動く」の代わりに、リセット後状態・正常入力の出力・停止中の保持・不許可入力の扱い・完了時点など、具体的な主張を書きます。各主張に一つ以上のテストと観測点を結ぶと、抜けた条件を見つけやすくなります。

独立した参照モデルが必要な理由

シフト RTL と同じスライス^{iスライス ベクトルから連続するビット範囲を選ぶ演算です。選択範囲が結果の幅とビット順を定めます。 詳しく見る}を参照モデルに写すと、インデックスの誤りも写す場合があります。整数の乗算・剰余や文字列の末尾比較など、別表現で仕様を実装すると相互確認に役立ちます。ただし表現が違うだけで独立性が証明されるわけではないので、小例を手で確認します。

カバレッジは通過回数ではありません

コード行が実行されたことと、機能条件を検査したことは異なります。reset×enable、state×input、full×push×pop などの交差条件が誤りを示す場合があります。ランダムだけに任せず、まれで重要な組合せを指向性テストで加えてください。

入力 N 個の組合せ回路は $2^N$ 組を全数検査できますが、順序回路には入力の時間列もあります。状態の到達可能性と、全遷移で不変条件^{i不変条件 許可されたすべての実行で、常に真でなければならない条件です。例えば深さ 4 の FIFO の格納数は常に 0 以上 4 以下です。}が保たれるかを解析します。有限のシミュレーション通過記録を、無制限時間の数学的証明と表現してはいけません。

実装を写した期待値ではなく、仕様から独立して正解を作ります。失敗時は実値だけでなく、直前の入力と状態も記録します。

失敗を小さくして記録する

最初の不一致の以前の状態・入力・期待値・実値を保存します。不要な刺激を減らして最小反例にしてから修正します。修正したテストだけでなく、既存の境界・リセット^{iリセット 状態を仕様で定めた初期値に戻す制御です。同期式か非同期式か、他の制御より優先されるかを合わせて定めます。 詳しく見る}検査も回帰実行してください。