// credit_counter_fv.sv — formal wrapper with properties
module credit_counter_fv (
  input logic clk, rst, inc, dec    // top-level inputs are left FREE by the tool
);
  logic [3:0] credits;

  credit_counter #(.MAX(12)) dut (.*);

  // Every trace starts in reset (open-source flow; commercial tools use a reset command)
  initial assume (rst);

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

  // The requirement: credits stay in the legal range 0..MAX
  a_in_range: assert property (credits <= 4'd12);

  // Something we want to SEE: the counter reaching zero at all
  c_empty:    cover  property (credits == 4'd0);
endmodule