min.sby

[options]
mode prove

[engines]
smtbmc z3

[script]
read -formal min.v
prep -top min

[files]
min.v

min.v

module min(
    input i_clk,
    input i_clk_en
    );

    reg [1:0] counter = 0;
    wire [1:0] next_counter;
    assign next_counter = counter + 1;

    always @(posedge i_clk) begin
        if (i_clk_en) begin
            counter <= next_counter;
        end
    end

    `ifdef FORMAL
    reg f_past_valid = 0;
    reg [1:0] f_past_next_counter;

    always @(posedge i_clk) begin
        if (i_clk_en) begin
            f_past_valid <= 1;
            f_past_next_counter <= next_counter;
            assert(~f_past_valid || counter == f_past_next_counter);
        end
    end
    `endif

endmodule