// updown_fv.sv — shows how an over-constraint hides the bug
module updown_fv (input logic clk, rst, up, down);
  logic [3:0] cnt;
  updown dut (.*);

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

  // "Upstream never does both" -- convenient, but is it TRUE?
  m_not_both: assume property (!(up && down));

  a_both_hold: assert property (up && down |=> $stable(cnt));   // PROVEN... vacuously
  a_up:        assert property (up && !down |=> cnt == $past(cnt) + 4'd1);
  a_down:      assert property (down && !up |=> cnt == $past(cnt) - 4'd1);

  // The defence: cover the antecedents
  c_both:      cover property (up && down);                        // UNREACHABLE -> red flag
endmodule