実習：カウンタのリセット・循環・不変条件の検証

実験対象と観測条件

初期値を 3 とし、最初の立上りエッジ^{i立上りエッジ クロックが 0 から 1 に変わる瞬間です。CLK=1 の区間全体を指すレベルとは区別します。 詳しく見る}でリセット^{iリセット 状態を仕様で定めた初期値に戻す制御です。同期式か非同期式か、他の制御より優先されるかを合わせて定めます。 詳しく見る}します。その後は 0、1、2、3、0 と進みます。リセット信号が有効でも、クロックエッジ前の値はそのままです。

始める前に

Digital Design Studio の Desktop プロジェクトと、正常に実行できる権限を用意してください。各例は別フォルダの rtl/top.sv に保存します。

SystemVerilog ソース

module top (
    input logic clk,
    input logic rst,
    output logic [1:0] count
);
    // Active-high synchronous reset: sampled only at the rising clock edge.
    always_ff @(posedge clk)
        if (rst) count <= 2'b00;
        else count <= count + 2'b01;
endmodule

実行方法

New analysis で Two-state single-clock v1 を選びます。Clock port は clk、周期は 1000ps です。次の設定で Preflight、Run RTL simulation を実行し、結果を比べてください。

入力刺激

[
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  }
]

下の各列は一つの立上りエッジの記録です。入力はエッジ直前、「更新後」の状態は更新直後です。並びはサンプル順で、物理的な伝搬遅延^{i伝搬遅延 入力が変わってから、出力が正しい値に安定するまでの時間です。論理式の等価性と時間特性は別の性質です。 詳しく見る}ではありません。E0～E4 は、それぞれ 500、1500、2500、3500、4500ps の立上りエッジです。最終値だけでなく、途中の count の列もすべて比較します。

結果の比較

5 cycles · count=00。500、1500、2500、3500、4500ps で 00 → 01 → 10 → 11 → 00 を確認してください。

この実習は 0/1 の単一クロック RTL を使い、#delay・initial・X/Z のテストベンチは含みません。学習完了の表示は学習記録であり、実際のシミュレーション結果ではありません。

期待状態をエッジ単位で計算します

初期レジスタ^{iレジスタ 複数ビットの状態を記憶する回路です。このコースの同期式レジスタは、クロックエッジで定められた入力を記憶します。 詳しく見る}値は 3 ですが、最初の立上りエッジではリセットが優先されます。初期化とリセットを同じものとして扱わないでください。

リセットのない区間では、各エッジで次の関係が成り立ちます。

最終値 00 だけでは、途中で誤った値を通っても検査を通過する場合があります。状態列全体とリセットの優先順位を別々に検査してください。

一度に一つずつ実験条件を変えます

• 初期値を 00 にしても、最初のリセット後の状態列は同じです。これでリセットが初期値に依存しないか確かめます。
• Reset cycles を 2 にすると、最初の二つの立上りエッジ後の count はともに 00 でなければなりません。その後の増加開始は一エッジ遅れます。
• 幅を 3 ビットへ広げると、循環周期は 8 回の増加です。宣言だけでなく、定数幅・初期レジスタ配列・実行長も確認します。

modulo-10 の設計へ一般化する

4 ビットの記憶は 0～15 を表すので、単純な増加だけでは 9 の次に 0 になりません。次状態関数を別に定めます。

この定義は未使用状態 10～15 で enable が有効になると 0 に戻します。別の回復方針も可能ですが、仕様と検証モデルは同じ方針を使う必要があります。