// watchdog_fv.sv — properties that do not depend on the exact count
module watchdog_fv (input logic clk, rst, start, kick, stop);
  logic bark;
  watchdog #(.TW(20)) dut (.*);

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

  // BARK is only entered from a quiet ARMED cycle (no stop, no kick)
  a_bark_quiet:     assert property ($rose(bark) |-> $past(!stop && !kick));
  a_stop_silences:  assert property (stop |=> !bark);
  a_bark_sticky:    assert property (bark && !stop |=> bark);
  c_bark:           cover  property (bark);   // with the cut: a few cycles; without: ~2^20
endmodule
// Tool command (vendor-specific), e.g.:  cut  dut.expired   /  stopat dut.expired