// Rule: once din has been stable for 4 clock edges, dout equals din.
// Written with a helper counter (stab) in the block below; the lab engine reads this form.
module debounce (input clk, input rst, input din, output reg dout);
  // dout follows din once din has been stable for 4 cycles
  reg [2:0] cnt;
  always @(posedge clk)
    if (rst) begin
      cnt <= 3'd0; dout <= 1'b0;
    end else if (din == dout) begin
      cnt <= 3'd0;
    end else if (cnt == 3'd4) begin          // bug: should be 3
      dout <= din; cnt <= 3'd0;
    end else begin
      cnt <= cnt + 3'd1;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // helper: for how many clock edges in a row din has kept its value
  reg       prev = 1'b0;
  reg [3:0] stab = 4'd0;
  always @(posedge clk) begin
    prev <= din;
    stab <= (rst || din != prev) ? 4'd0 : (stab == 4'd15 ? stab : stab + 4'd1);
  end
  // once din has been stable for 4 edges, dout has followed it
  always @(posedge clk) if (!init && stab >= 4'd4 && din == prev) assert (dout == din);
`endif
endmodule