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