// Checker for {dut_name}
// Auto-generated by GenerateChecker tool
// Source RTL: {rtl_file_path}

module {dut_name}_checker{param_decl} (
  {port_decl}
);

  // ---------------------------------------------------------------------------
  // 0. Default Clocking & Disable (simplifies SVA — no need to repeat @(posedge clk))
  // ---------------------------------------------------------------------------
  default clocking cb @(posedge clk); endclocking
  default disable iff (!rst_n);

  // ---------------------------------------------------------------------------
  // 1. Auxiliary Logic & Internal Reset
  // ---------------------------------------------------------------------------
  // [LLM-TODO-1]: Define auxiliary wires/regs for complex property construction.
  // Example: wire is_bypass = empty & write_valid & read_ready;

  // ---------------------------------------------------------------------------
  // 2. FG-ENVIRONMENT: Assumptions & Protocol Constraints
  // ---------------------------------------------------------------------------
  // Define input stability and interface protocol constraints here.
  // Example: !io_ready |-> $stable(io_valid) && $stable(io_data)

  // 【重要】如果设计使用符号化索引 (fv_idx)，必须添加以下约束以防止假阳性：
  // 请参考 Guide_Doc/dut_property_template.md 中的"模式 3：符号化索引与单点修改保证"
  //
  // <CK-FV-IDX-STABLE> (Style: Assume) 符号化索引稳定性约束
  // property CK_FV_IDX_STABLE;
  //   @(posedge clk) disable iff (!rst_n)
  //   $stable(fv_idx);
  // endproperty
  // M_CK_FV_IDX_STABLE: assume property (CK_FV_IDX_STABLE);
  //
  // <CK-FV-IDX-VALID> (Style: Assume) 符号化索引范围约束
  // 注意：不要使用 disable iff，确保复位期间也有效
  // property CK_FV_IDX_VALID;
  //   @(posedge clk)
  //   fv_idx < NUM_PORTS;  // 替换 NUM_PORTS 为实际的数组大小参数
  // endproperty
  // M_CK_FV_IDX_VALID: assume property (CK_FV_IDX_VALID);
  //
  // <CK-FV-IDX-KNOWN> (Style: Assume) 符号化索引非X态约束
  // property CK_FV_IDX_KNOWN;
  //   @(posedge clk)
  //   !$isunknown(fv_idx);
  // endproperty
  // M_CK_FV_IDX_KNOWN: assume property (CK_FV_IDX_KNOWN);

  // ---------------------------------------------------------------------------
  // 3. FG-CONTROL: State Machines, Pointers, and Flags
  // ---------------------------------------------------------------------------
  // Verify state transitions, pointer increments, and status flags (Full/Empty).

  // ---------------------------------------------------------------------------
  // 4. FG-DATAPATH: Data Integrity & Bypass
  // ---------------------------------------------------------------------------
  // Verify data movement, storage consistency (using fv_idx), and bypass paths.

  // ---------------------------------------------------------------------------
  // 5. FG-PROGRESS: Liveness & No-Starvation
  // ---------------------------------------------------------------------------
  // Ensure "something good eventually happens".
  // Example: (valid && !ready) |-> s_eventually ready;

  // ---------------------------------------------------------------------------
  // 6. FG-COVERAGE: Reachability Covers
  // ---------------------------------------------------------------------------
  // PROOF OF REACHABILITY: Mandatory covers to avoid TRIVIALLY_TRUE passes.
  // Example: cover property (@(posedge clock) full == 1'b1);

endmodule
