`default_nettype none

module test (i_clk, i_wr, i_val, i_rst, o_match);

input i_clk;
input i_wr;
input i_val;
input i_rst;
output o_match;

reg r_val;

always @(posedge i_clk) begin
    if (i_rst) begin
        r_val <= 1'b0;
    end
    else if (i_wr) begin
        r_val <= i_val;
    end
end

assign o_match = (r_val == i_val);

endmodule






module test_tb();

reg clk;
reg wr;
reg val;
reg rst;
wire match1;
wire match2;

initial begin
    rst <= 1'b1;
    wr <= 1'b1;
    val <= 1'b1;
    #1000 rst<= 1'b0;
end

`ifdef FORMAL
    reg f_last_clk;
    always @($global_clock) begin
        assume(clk == !f_last_clk);
        f_last_clk <= clk;
        clk <= (clk === 1'b0);
    end

    reg f_past_valid;
    initial f_past_valid = 1'b0;
    always @(posedge clk) begin
        f_past_valid <= 1'b1;
    end

    always @(posedge clk) begin
        if (!f_past_valid) begin
            assume(rst);
        end
        if (!rst) begin
            assert (match1 == match2);
        end
    end
`else
    always #100 clk <= (clk === 1'b0);
`endif

test test1 (
    .i_clk(clk),
    .i_wr(wr),
    .i_val(val),
    .i_rst(rst),
    .o_match(match1)
);

test test2 (
    .i_clk(clk),
    .i_wr(wr),
    .i_val(val),
    .i_rst(rst),
    .o_match(match2)
);

endmodule