6.2 時鐘域標註與 unsafe(cdc) 檢查#

從「物理問題」到「語言問題」#

上一節的結論是嚴峻的：在 SystemVerilog 裡，六種常見的 CDC 錯誤全部是合法程式碼。編譯器不會說一句話，模擬器永遠給出正確波形，唯一的防線是外部 CDC 工具（Spyglass、Questa CDC、Synopsys SpyGlass CDC 等）與 code review 的人肉紀律。

這個現狀的問題結構，與本書第 4.2 節處理過的「時脈極性」問題同構：

• 時脈極性問題：「這根線是時脈」這個資訊只存在於命名慣例裡，因此工具無法檢查，Veryl 的解法是把它放進型別（clock / reset）。
• CDC 問題：「這根線屬於哪個時鐘域」這個資訊只存在於工程師的腦中與註釋裡，因此編譯器無法檢查，Veryl 的解法是把它放進語法。

Veryl 的答案由兩個機制組成：

1. 時鐘域標註：用 'a 這樣的識別碼宣告每個訊號屬於哪個域；
2. 跨域檢查與 unsafe (cdc) 豁免：凡是跨域的賦值都是編譯錯誤，除非設計者明確寫出 unsafe (cdc)。

這一章我們逐項拆解這兩個機制，並在最後誠實地討論這個設計不能做什麼。

時鐘域標註語法#

基本形式#

Veryl 在埠與訊號的型別前用一個前引號的識別碼標註時鐘域：

module Bridge (
    i_clk_a : input 'a clock,
    i_rst_a : input 'a reset,
    i_dat_a : input 'a logic<8>,

    i_clk_b : input 'b clock,
    i_rst_b : input 'b reset,
    o_dat_b : output 'b logic<8>,
) {
}

'a 與 'b 是時鐘域識別碼。它們不是型別、不是參數，而是附加在訊號上的域屬性：i_dat_a 屬於域 'a，o_dat_b 屬於域 'b。域識別碼在同一個模組內只需一致即可，不同模組之間的 'a 互不干涉。

何時必須標註#

Veryl 的規則是：

這條規則的取捨很清楚：絕大多數模組是單時脈的（一個模組內部同時存在多個時脈本來就是應該警惕的設計），強迫它們全部標註會讓程式碼噪音化；但一旦你在一個模組裡放了第二個時脈，你就進入了 CDC 的雷區，語言要求你把每根線的域歸屬說清楚——這正是 6.1 節錯誤一到錯誤六的共同根源（資訊不在程式碼裡）。

換句話說：單時脈模組的簡潔性與多時脈模組的顯式性，在 Veryl 裡是同一條規則的兩面。

域的推斷#

標註埠之後，模組內部訊號的域不需要逐一宣告——Veryl 會從賦值語境推斷。

從 assign 推斷#

module Bridge (
    i_clk_a : input 'a clock,
    i_dat_a : input 'a logic<8>,
) {
    var r_buf : logic<8>

    assign r_buf = i_dat_a;   // r_buf 被推斷為屬於 'a
}

r_buf 在 assign 的左側、右側來源是 'a 域的訊號，於是 r_buf 屬於 'a。推斷規則很簡單：組合賦值的左側繼承右側的域。

從 always_ff 的時脈推斷#

module Bridge (
    i_clk_b : input 'b clock,
    i_rst_b : input 'b reset,
    i_dat   : input 'b logic<8>,
) {
    var r_q : logic<8>

    always_ff (i_clk_b, i_rst_b) {
        if_reset {
            r_q = 0;
        } else {
            r_q = i_dat;
        }
    }
    // r_q 被推斷為屬於 'b：它的值由 clk_b 域的時脈驅動
}

在 always_ff (i_clk_b) 中被賦值的變數屬於 'b——這在物理上就是事實：這顆 FF 的時脈端接的是 clk_b，它的輸出就是 clk_b 域的訊號。推斷不是猜測，是把物理事實形式化。

介面實例也可帶域#

inst u_if : 'a InterfaceA;

介面實例上標註 'a，表示這個介面內的所有訊號屬於域 'a。介面是 SoC 設計中訊號最密集的地方（一個 AXI 介面有數十根訊號），能夠以實例為單位標註域，避免了逐根訊號重複標註的噪音。

推斷的意義#

域推斷的價值在於讓標註成本集中在新資訊上。設計者只需要在「域的邊界」——也就是埠與時脈——標註一次，內部邏輯的域歸屬由編譯器推導。這與型別推斷的哲學一致：人類只寫有資訊量的東西，機器推導可推導的東西。

跨域檢查與 unsafe (cdc)#

跨域賦值是編譯錯誤#

現在來看這套機制的核心。以下程式碼嘗試把 'a 域的訊號直接賦給 'b 域：

module Bridge (
    i_clk_a : input 'a clock,
    i_dat_a : input 'a logic<8>,

    i_clk_b : input 'b clock,
    o_dat_b : output 'b logic<8>,
) {
    assign o_dat_b = i_dat_a;   // 編譯錯誤：跨域賦值
}

這是編譯錯誤，不是警告。 Veryl 的編譯器會報告「這是一個跨時鐘域賦值」，並指出兩側的域識別碼。

回顧 6.1 節的錯誤一：這正是那個「模擬永遠正確、矽上隨機出錯」的原始錯誤。在 SystemVerilog 裡，抓出它需要買一套 CDC lint 工具、配置時鐘域檔案、跑完整個專案的掃描、然後在數千條報告裡過濾真陽性。在 Veryl 裡，它是編譯不過——你根本無法產生一份含有未同步跨域的 SystemVerilog。

豁免：unsafe (cdc)#

當然，跨域是有意為之的設計行為——同步器本身、非同步 FIFO、握手橋，全都是「合法的跨域」。語言不可能禁止跨域，它要做的是強制你意識到自己正在跨域。Veryl 的機制是 unsafe (cdc) 區塊：

module Bridge (
    i_clk_a : input 'a clock,
    i_dat_a : input 'a logic<8>,

    i_clk_b : input 'b clock,
    i_rst_b : input 'b reset,
    o_dat_b : output 'b logic<8>,
) {
    var r_sync1 : logic
    var r_sync2 : logic

    always_ff (i_clk_b) {
        r_sync1 = i_dat_a;
        r_sync2 = r_sync1;
    }

    unsafe (cdc) {
        assign o_dat_b = {r_sync2, r_sync2, r_sync2, r_sync2};
    }
}

語意是：「我知道這裡有跨域，我已經做了同步處理，責任在我。」 編譯器放行，但這個決定被永久記錄在程式碼裡。

unsafe 的設計哲學：責任的顯式轉移#

這裡有一個值得深入討論的命名選擇：為什麼叫 unsafe 而不是 ignore 或 allow？

這借鑑了 Rust 的 unsafe 機制，其核心思想是：

unsafe 不是「關閉檢查」，而是「把責任從工具顯式轉移到設計者與 code review」。

比較三種可能的設計：

unsafe 這個詞的選擇是刻意的：它在字面上就宣告「這裡的檢查被繞過了，這段程式碼的安全由人來保證」。工程上的直接後果是：

1. grep 即審查：grep -rn "unsafe (cdc)" src/ 列出專案中所有的跨域點。一個十萬行的專案，跨域點通常是個位數到數十位數——這就是你的 CDC 審查清單。
2. code review 流程整合：任何 PR 中新增或修改的 unsafe (cdc) 都應該是 review 的必查項。可以進一步在 CI 中加一道檢查：unsafe (cdc) 的數量相對於基線增加時，要求 PR 明確說明。
3. 防止「無意識擴散」：因為每個跨域點都需要打字寫出 unsafe (cdc)，工程師不會在順手之間擴散跨域邏輯。

一個實際的審查清單建議（放進團隊的 review checklist）：

• 這個 unsafe (cdc) 對應的同步器是幾級？
• 同步器的第一級是否直接面對源域 FF 的輸出（中間無組合邏輯，6.1 節錯誤三）？
• 若是多位元：是否用了格雷碼、握手或 FIFO，而不是逐位元同步（6.1 節錯誤四）？
• 是否已加 #[sv(...)] 屬性防止同步器被優化（6.1 節錯誤五）？
• 這個跨域點在 veryl doc 產生的文件裡是否有說明？

unsafe 區塊內可放整個模組實例#

跨域邊界經常要例項化一個現成的同步元件（可能來自 $sv:: 命名空間的既有 IP）。unsafe (cdc) 支援包裹整個實例：

unsafe (cdc) {
    inst u_sync: $sv::SynchronizerCell (
        i_clk   : i_clk_b,
        i_async : i_dat_a,
        o_sync  : w_dat_b,
    );
}

這個形式表達的語意很精確：「這個例項本身就是跨域邊界。」 對 CDC 審查而言，這比「跨域藏在模組內部某處」好得多——邊界在結構上可見。

與 lint 檢查的整合#

要區分 Veryl 的兩層檢查機制：

CDC 檢查在第一層，這是深思熟慮的：跨域不是風格問題，是正確性問題，所以它不能像 lint 那樣被輕易抑制——豁免必須用語法上更重的 unsafe (cdc) 區塊。

生成的 SystemVerilog：語言保真度的取捨#

一個誠實的觀察：unsafe (cdc) 與 'a 標註在生成的 SystemVerilog 中不留任何痕跡。

// Veryl
unsafe (cdc) {
    assign o_dat_b = w_dat_b;
}

// 生成的 SystemVerilog
assign o_dat_b = w_dat_b;

原因很直接：SystemVerilog 沒有時鐘域的概念，無處安放這個資訊。這是本書反覆出現的「語言保真度」議題的又一案例：

• 4.2 節的 clock_edge / reset_type：建置設定不留在 SV 裡，讀 SV 的人需要看 Veryl.toml；
• 本節的 'a 與 unsafe (cdc)：域資訊不留在 SV 裡，讀 SV 的人需要看 Veryl 原始碼。

這個取捨的方向是一致的：Veryl 把「設計意圖」保留在自己的原始碼層，生成的 SV 只承載「電路事實」。 這意味著：如果你的下游流程（review、ECO、形式驗證）工作在生成的 SV 上，你會失去 CDC 檢查的能力；只有回到 Veryl 原始碼層，域檢查才存在。這正是「以 Veryl 原始碼為單一真相來源（single source of truth）」的專案組織方式的又一個論據——我們在第 2.2 節（.sv.map）已經見過同樣的邏輯。

設計討論#

價值：把 CDC 從紀律變成編譯器#

比較兩種世界：

最大的質變是檢查發生的時刻。SystemVerilog 流程裡，CDC 檢查是「事後稽核」——你先寫完整個設計，再掃描；發現問題時，修改已經擴散。Veryl 的檢查是「寫下即攔截」——你在寫跨域賦值的那一刻就被擋住，此時上下文還在腦中，修正成本最低。這與「在 CI 攔 bug」與「在編譯器攔 bug」的差別同構：越早的檢查，越便宜。

取捨：語言能強制你思考，不能替你思考#

必須誠實地指出這套機制的邊界：

unsafe (cdc) 只能判定「這裡有跨域」，不能判定「這個跨域是安全的」。

具體地說，編譯器不知道：

1. 你的同步器是幾級、MTBF 是否足夠；
2. 你同步的是單位元還是多位元（unsafe (cdc) 區塊裡照樣可以寫出逐位元同步的錯誤）；
3. 格雷碼指標的單調性是否真的成立（那是形式驗證的領域，見 6.3 節）。

這是所有靜態檢查的根本限制：語言檢查能做的是「強制你在每個跨域點停下手來思考」，而不是「替你判斷這個跨域對不對」。 因此 6.1 節說的三層防線在 Veryl 的世界裡依然全部成立——語言層檢查取代的是「外部 CDC lint」的位置，形式驗證與實體驗證的位置沒有任何改變。

換一個角度說：Veryl 把 CDC 從「靠 code review 紀律維持」變成了「靠編譯器維持下限、review 專注上限」。紀律會疲勞、會隨團隊規模劣化；編譯器不會。

實作練習#

練習一：讓編譯器找出跨域#

題目： 以下是 SystemVerilog 的跨域橋接器（刻意含錯）。將它改寫成 Veryl，讓編譯器找出所有跨域賦值，然後用正確的同步器修復。

module CdcBridge (
    input  logic       clk_a,
    input  logic [7:0] data_a,
    input  logic       valid_a,

    input  logic       clk_b,
    input  logic       rst_n_b,
    output logic [7:0] data_b,
    output logic       valid_b
);
    // 錯誤一：valid_a 直接跨域
    // 錯誤二：data_a 逐位元同步（多位元 skew）

    logic [7:0] data_sync;
    logic       valid_sync1, valid_sync2;

    always_ff @(posedge clk_b or negedge rst_n_b) begin
        if (!rst_n_b) begin
            valid_sync1 <= 1'b0;
            valid_sync2 <= 1'b0;
        end else begin
            valid_sync1 <= valid_a;
            valid_sync2 <= valid_sync1;
        end
    end

    always_ff @(posedge clk_b) begin
        data_sync <= data_a;    // 未同步的直接賦值
    end

    assign data_b  = data_sync;
    assign valid_b = valid_sync2;
endmodule

提示： 正確的架構是「握手」——資料在源域鎖存後穩定不動，只有一個 1-bit 的 req（或 valid）跨域同步；目的域同步到 req 之後取樣資料匯流排，回一個 ack 跨域同步回源域。資料匯流排在 req 穩定期間是靜止的，因此即使不逐位元同步，也不存在 skew 問題——這就是握手協定能安全傳多位元資料的原因（6.3 節完整實作）。

練習二：觀察 unsafe 的可搜尋性#

題目： 完成練習一後，對專案執行：

grep -rn "unsafe (cdc)" src/

觀察輸出：你應該看到恰好兩個豁免點——req 的跨域同步與 ack 的跨域同步。想像這個專案有十萬行、三十個跨域點：這條 grep 命令就是你的 CDC 審查地圖。

思考： 在原來的 SystemVerilog 版本中，你如何回答「這個專案有幾個跨域點」這個問題？

本章小結#

1. Veryl 用 'a 這樣的時鐘域識別碼把「這根線屬於哪個域」放進語法；模組內有多個時脈時必須標註，單時脈可用隱式域 '_。
2. 域可以從賦值語境推斷：assign 左側繼承右側的域；always_ff (i_clk_b) 中賦值的變數屬於 'b；介面實例可整體標註 inst u_if : 'a InterfaceA;。
3. 跨域賦值是編譯錯誤；豁免必須用 unsafe (cdc) 區塊——它把責任顯式轉移到設計者，並留下可 grep 的風險標記。
4. unsafe 的命名是刻意的（借鑑 Rust）：不是「關閉檢查」，是「責任顯式轉移」。審查流程應把 unsafe (cdc) 列入必查清單。
5. unsafe (cdc) 可包裹整個模組實例，把「跨域邊界」結構化地標示出來。
6. 域檢查與 lint 是兩層機制：跨域是編譯錯誤（正確性），lint 是警告（意圖完整性）。
7. 語言能做的是強制你思考每個跨域點，不能替你思考這個跨域是否安全——形式驗證與實體驗證的地位不變。
8. 'a 與 unsafe (cdc) 在生成的 SV 中不留痕跡——設計意圖保留在 Veryl 層，這是「以 Veryl 為單一真相來源」的又一論據。

下一節（6.3）我們進入實作層：2-FF 同步器的完整 Veryl 實作與 MTBF 分析、格雷碼的完整推導、四相與二相握手協定、以及非同步 FIFO 的完整實作與驗證策略。

下一節：第 6.3 節「同步器的實作、驗證與協議（MTBF）」