カウンタのデバッグと最小反例

最終値が正しくても順序は誤っているかもしれません

カウンタが 0 で終わっただけでは、reset と循環が正しいと結論できません。ずっと 0 に止まる回路も同じ結果になります。正常な増加・保持・リセット^{iリセット 状態を仕様で定めた初期値に戻す制御です。同期式か非同期式か、他の制御より優先されるかを合わせて定めます。 詳しく見る}・境界での循環を、それぞれ示す観測点が必要です。

二つの機能を意図的に競合させる

制御を一つずつ試すだけでは、優先順位の誤りを見つけにくくなります。

下の各列は立上りエッジ^{i立上りエッジ クロックが 0 から 1 に変わる瞬間です。CLK=1 の区間全体を指すレベルとは区別します。 詳しく見る}の記録です。入力はエッジ直前、「更新後」の状態は更新直後です。並びはサンプル順で、物理的な伝搬遅延^{i伝搬遅延 入力が変わってから、出力が正しい値に安定するまでの時間です。論理式の等価性と時間特性は別の性質です。 詳しく見る}ではありません。初期 count=5 です。誤った回路は enable の内側でしか reset を調べないので、最初のエッジで 5 を保持します。最終値が同じでも、最初の不一致が不具合を示します。

modulo-8 の参照回路を初期 101 から始めます。enable=0、reset=1 を選んでクロックを進めてください。正解は 000 です。reset を enable の内側に置いた誤 RTL は 101 を保持します。reset 解除後、enable=0 の保持と enable=1 の増加も区別します。

参照モデルで最初の不一致を探す

この式は正常状態 0～M-1 を前提にした機能モデルです。範囲外からの回復は別方針として加えます。各エッジの期待値を計算して実値と比べてください。最初の不一致の直前の入力と状態が、原因を探す最小の出発点です。

1000 サイクル後に失敗したなら、不要な入力区間を削り、同じ誤りを 3～5 エッジで再現してみます。RTL 修正後、その最小反例を回帰テストに残します。設計とテストを同じ誤条件に変えないよう、修正した仕様とコードを別々に確認します。