實作：驗證計數器的重設、回捲與不變量

實驗對象與觀察條件

初值設為 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上升緣是時脈由 0 變成 1 的瞬間。它與表示整段 CLK=1 期間的高準位不同。 詳細內容}的觀察紀錄。輸入為邊緣前值，名稱含「後」的狀態為更新後值。欄位對齊表示取樣順序，並未繪出實體傳播延遲^{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 位元時，回捲週期為八次遞增。除了宣告，也要檢查常數寬度、初始暫存器陣列與執行長度。

推廣到 modulo-10 設計

4 位元儲存空間表示 0～15，因此單純遞增不會在 9 之後變成 0，必須另外定義下一狀態函數。

此定義會在未使用狀態 10～15 收到 enable 時回到 0。也可採用其他復原策略，但規格與驗證模型必須使用相同策略。