module sat_counter (input clk, input rst, input en, output reg [3:0] q);
  always @(posedge clk)
    if (rst)                    q <= 4'd0;
    else if (en && q != 4'd12)  q <= q + 4'd1;
endmodule

// Formal wrapper for sat_counter. The lab checks sat_counter_formal_top automatically
// when this file exists; keep Top Module set to sat_counter.
// SVA form (with bind, in commercial tools): assert property (@(posedge clk) disable iff (rst) q <= 4'd12);

module sat_counter_formal_top (
    input clk,
    input rst,
    input en,
    output [3:0] q
);

    sat_counter u_dut (
        .clk(clk),
        .rst(rst),
        .en(en),
        .q(q)
    );

    initial assume (rst == 1'b1);   // start in reset

    always @(posedge clk) begin
        if (!rst) begin
            assert (q <= 4'd12);
        end
    end

endmodule