Solutions to problems 1 and 2

// gray_counter.sv
module gray_counter #(
  parameter int W = 4
) (
  input  logic         clk, rst, en,
  output logic [W-1:0] gray
);
  logic [W-1:0] bin;
  always_ff @(posedge clk)
    if (rst)     bin <= '0;
    else if (en) bin <= bin + 1'b1;
  assign gray = bin ^ (bin >> 1);
endmodule

// 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

// pulse_stretch.sv
module pulse_stretch #(
  parameter int N = 4
) (
  input  logic clk, rst, in_pulse,
  output logic out
);
  localparam int CW = $clog2(N + 1);
  logic [CW-1:0] cnt;
  always_ff @(posedge clk)
    if (rst)              cnt <= '0;
    else if (in_pulse)    cnt <= CW'(N);       // (re)start the window
    else if (cnt != '0)   cnt <= cnt - 1'b1;
  assign out = (cnt != '0);
endmodule

// pulse_stretch_fv.sv
module pulse_stretch_fv #(
  parameter int N = 4
) (
  input logic clk, rst, in_pulse
);
  logic out;
  pulse_stretch #(.N(N)) dut (.*);

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

  a_on_for_n:  assert property (in_pulse |=> out [*N]);
  a_off_after: assert property (in_pulse ##1 (!in_pulse) [*N] |=> !out);
  a_cause:     assert property ($rose(out) |-> $past(in_pulse));

  c_retrigger: cover property (in_pulse ##2 in_pulse ##1 out [*N-1]);
endmodule