// decade_counter_fv.sv
module decade_counter_fv (input logic clk, rst, en);
  logic [3:0] cnt;
  decade_counter dut (.*);

  initial assume (rst);
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  // True, but NOT inductive on its own:
  a_never_12: assert property (cnt != 4'd12);

  // Helper invariant: inductive, and it implies a_never_12
  a_range:    assert property (cnt <= 4'd9);
endmodule