pinmux_x_path_checker systemverilog

pinmux_x_path_checker.sv

// pragma translate_off
// Checker module: verifies that when pinmux select is high, any X value
// from the module output must propagate to the corresponding GPIO within
// a given cycle latency window. Otherwise, it triggers a fatal error.
module pinmux_x_path_checker #(
  parameter int MIN_LAT = 1,     // Minimum cycle delay allowed
  parameter int MAX_LAT = 8,     // Maximum cycle delay allowed
  parameter int WIDTH   = 1      // Data width (1 = single bit)
)(
  input  logic                 clk,
  input  logic                 rst_n,       // Reset, used for disable iff
  input  logic                 pinmux_sel,  // When high, module output is connected to GPIO
  input  logic [WIDTH-1:0]     mod_out,     // Module output signal
  input  logic [WIDTH-1:0]     chip_gpio    // Corresponding chip GPIO
);

  // Strict "all bits are X" function (does not treat Z as X)
  function automatic bit is_all_x (logic [WIDTH-1:0] v);
    return (v === 'bx); // Returns 1 only if *all* bits are X
  endfunction

  // Property: if pinmux_sel is high and module output is all X,
  // then within MIN_LAT..MAX_LAT cycles, GPIO must also be all X.
  property p_x_propagates_through_pinmux;
    @(posedge clk) disable iff (!rst_n)
      (pinmux_sel && is_all_x(mod_out))
      |-> ##[MIN_LAT:MAX_LAT] is_all_x(chip_gpio);
  endproperty

  // Assertion: fails immediately if property is violated
  a_x_propagates_through_pinmux: assert property (p_x_propagates_through_pinmux)
    else $fatal(1,
      $sformatf("X did not propagate to chip_gpio within %0d..%0d cycles when pinmux_sel=1",
                MIN_LAT, MAX_LAT)
    );

  // Optional cover: ensures we actually observe X propagation in sim
  c_x_seen_on_gpio: cover property (
    @(posedge clk) disable iff (!rst_n)
      (pinmux_sel && is_all_x(mod_out)) ##[MIN_LAT:MAX_LAT] is_all_x(chip_gpio)
  );

endmodule
// pragma translate_on

bind your_soc_top pinmux_x_path_checker #(
  .MIN_LAT(1),
  .MAX_LAT(4),
  .WIDTH  (1)
) u_chk_gpio17 (
  .clk        (tb_clk),
  .rst_n      (tb_rst_n),
  .pinmux_sel (dut.pinmux.gpio17_sel),
  .mod_out    (dut.u_block.sig_out),
  .chip_gpio  (dut.pad_ring.gpio[17])
);

幫我用systemverilog assert研究以下寫法:

sva 可做: 假設 pinmux select為真, 則當下若module port上的某output為 x, 下一cycle(隨便找一個 postsim也能meet的delay)在對應的chip gpio必為x, 不然就當場死掉
SystemVerilog ASIC Designer said:

太好了，這題就是 SVA 的主場。下面給你一個「可直接用/改」的寫法，重點是：

取樣在時脈邊緣（避免 race）。

允許「某個可達的延遲視窗」（##[MIN:MAX]）來涵蓋 post-sim 可滿足的延遲。

嚴格檢查 X（不是 Z）。要放寬成 X/Z 也一行就能換。

失敗就立刻 $fatal「當場死掉」。

1. 參數化的 property（嚴格 X 檢查）
   // pragma translate_off
   module pinmux_x_path_checker #(
   parameter int MIN_LAT = 1, // 允許的最小循環延遲
   parameter int MAX_LAT = 8, // 允許的最大循環延遲
   parameter int WIDTH = 1 // 資料位寬（1 表示單 bit）
   )(
   input logic clk,
   input logic rst_n, // 同步/非同步 reset 皆可，用作 disable iff
   input logic pinmux_sel, // 當此為 1 時，模組輸出被接到對應 GPIO
   input logic [WIDTH-1:0] mod_out, // module port 上的輸出
   input logic [WIDTH-1:0] chip_gpio // 對應的 chip GPIO
   );

// 嚴格「全為 X」的判斷，不把 Z 當成 X
function automatic bit is_all_x (logic [WIDTH-1:0] v);
return (v === 'bx); // 全部位元皆為 X 才會是 1；若含 Z 則為 0
endfunction

// 若你想把 X 或 Z 都當作 unknown，只要改成：$isunknown(v)
// function automatic bit is_unknown (logic [WIDTH-1:0] v);
// return $isunknown(v); // 任何位元含 X 或 Z 即為 1
// endfunction

// 當 pinmux_sel 為真且此 cycle 模組輸出為 X，
// 則在之後 MIN_LAT..MAX_LAT 的任一個 cycle，GPIO 必須也變成 X
property p_x_propagates_through_pinmux;
@(posedge clk) disable iff (!rst_n)
(pinmux_sel && is_all_x(mod_out))
|-> ##[MIN_LAT:MAX_LAT] is_all_x(chip_gpio);
endproperty

// 失敗就當場 $fatal
a_x_propagates_through_pinmux: assert property (p_x_propagates_through_pinmux)
else $fatal(1,
$sformatf("X did not propagate to chip_gpio within %0d..%0d cycles when pinmux_sel=1",
MIN_LAT, MAX_LAT)
);

// （選用）做個 cover 幫你看得到成功案例，debug 很實用
c_x_seen_on_gpio: cover property (
@(posedge clk) disable iff (!rst_n)
(pinmux_sel && is_all_x(mod_out)) ##[MIN_LAT:MAX_LAT] is_all_x(chip_gpio)
);

endmodule
// pragma translate_on

怎麼用？

若你預期「模組→pinmux→GPIO」最佳情況 1 cycle，最差 4 cycles，就用 MIN_LAT=1, MAX_LAT=4。

嚴格只認 X：用 is_all_x（如上）。

若要把 X 或 Z 都當 unknown，把 property 中 is_all_x(...) 換成 $isunknown(...) 即可。

2. 單點快速版（無模組化）

如果你就一個地方要檢查、也不想拉 module，直接 in-place：

// 假設以下信號皆在本 scope 可見
// logic clk, rst_n, pinmux_sel;
// logic [W-1:0] mod_out, chip_gpio;

property x_prop;
@(posedge clk) disable iff (!rst_n)
(pinmux_sel && (mod_out === 'bx)) |-> ##[1:8] (chip_gpio === 'bx);
endproperty

assert property (x_prop)
else $fatal(1, "X failed to show up on chip_gpio within 1..8 cycles while pinmux_sel=1");

3. 若需要 time-based（非整數 cycle）視窗

SVA 本質是 cycle-based，但你可以在一個「快時脈」下用多個 cycles 近似時間視窗；
或用 non-clocked property + ## 的時間延遲（工具支援度要確認）。範例：

// 非同步取樣（工具需支援 time-based SVA；常見 flow 還是建議用 clocked + 週期視窗）
default clocking cb @(posedge clk); endclocking

sequence within_ns(int tmin_ns, int tmax_ns);
##[tmin_ns1ns : tmax_ns1ns] 1;
endsequence

property p_time_window_x;
disable iff (!rst_n)
(pinmux_sel && (mod_out === 'bx)) |-> within_ns(2, 20) and (chip_gpio === 'bx);
endproperty

assert property (p_time_window_x)
else $fatal(1, "X did not reach GPIO within 2..20 ns");

如果工具對 time-based 序列支援不齊，建議改回 cycle 視窗，並以 STA/仿真估計最大/最小 pipeline 週期數。

4. 常見細節與坑位

方向/三態：若 GPIO 會 tri-state，且你不想把 Z 視為成功，就一定要用嚴格 === 'bx，不要用 $isunknown。

寬度不一致：多 bit bus 檢查「全為 X」用 bus === 'bx 最乾淨；如果你要的是「只要含有任一 X 就算」，可改成 |bus === 'bx（位元或再比對）或自寫函式掃描位元。

pinmux_sel 穩定性：若 sel 需要在整個視窗期間保持為 1，改寫為
(pinmux_sel && is_all_x(mod_out)) |-> (pinmux_sel throughout ##[MIN:MAX] 1) and ##[MIN:MAX] is_all_x(chip_gpio);
或把 pinmux_sel 包在 throughout。

reset 期間：disable iff (!rst_n) 可以避免 reset 亂流導致誤報。若你的 reset 為同步，改條件即可。

多個 GPIO/多路：把 checker 模組化後，用 generate 或 bind 套用到每一條 mux mapping。

5. 用 bind 套進現有 RTL（零侵入）
   // 在 testbench 或 top-level 驗證層加入：
   bind your_soc_top pinmux_x_path_checker #(
   .MIN_LAT(1),
   .MAX_LAT(8),
   .WIDTH (1)
   ) u_chk_gpio17 (
   .clk (tb_clk),
   .rst_n (tb_rst_n),
   .pinmux_sel (dut.pinmux.gpio17_sel),
   .mod_out (dut.u_myblock.out_sig),
   .chip_gpio (dut.pad_ring.gpio[17])
   );

想更狠一點？可以再加一條「反向」檢查：當 pinmux_sel=1 且 mod_out 不是 X 時，不應該在延遲視窗內看到 GPIO 為 X（避免外部噪聲注入到 pad）。同理可檢查 0/1 的值一致性。
需要我幫你把這組 checker 擴成「值一致（0/1/X/Z 可選）、可選保持 sel、可選脈衝寬度」的通用套件嗎？