// gray_counter_fv.sv
module gray_counter_fv #(
  parameter int W = 4
) (
  input logic clk, rst, en
);
  logic [W-1:0] gray;
  gray_counter #(.W(W)) dut (.*);

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

  a_one_bit: assert property (en  |=> $countones(gray ^ $past(gray)) == 1);
  a_hold:    assert property (!en |=> $stable(gray));

  // Largest Gray value (binary all ones) is 100...0; the next value wraps to 0
  localparam logic [W-1:0] GMAX = {1'b1, {(W-1){1'b0}}};
  c_wrap:    cover  property (gray == GMAX && en ##1 gray == '0);
endmodule