data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/counter_properties.sv
1: b"%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/counter_properties.sv:38: syntax error, unexpected property, expecting '#' or final\n    assume property (@(posedge clk_i) (!init) |-> !rst_ni);\n           ^~~~~~~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/counter_properties.sv:50: syntax error, unexpected |=>, expecting ')'\n        (count_up && !resetting) |=> q_o == $past(q_o) + {{WIDTH-1{1'b0}}, 1'b1});\n                                 ^~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/counter_properties.sv:55: syntax error, unexpected |=>, expecting ')'\n        (count_down && !resetting) |=> q_o == $past(q_o) - {{WIDTH-1{1'b0}}, 1'b1});\n                                   ^~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/counter_properties.sv:60: syntax error, unexpected |=>, expecting ')'\n        clear_i |=> q_o == '0);\n                ^~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/counter_properties.sv:65: syntax error, unexpected |=>, expecting ')'\n        (load_i && !clear_i) |=> q_o == $past(d_i));\n                             ^~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/counter_properties.sv:82: syntax error, unexpected |=>\n            (overflow_o && !resetting |=> overflow_o));\n                                      ^~~\n%Error: Exiting due to 6 error(s)\n"
module counter_properties #(
    parameter int unsigned WIDTH = 4,
    parameter bit STICKY_OVERFLOW = 1'b0
)(
    input logic             clk_i,
    input logic             rst_ni,
    input logic             clear_i,
    input logic             en_i,
    input logic             load_i,
    input logic             down_i,
    input logic [WIDTH-1:0] d_i,
    input logic [WIDTH-1:0] q_o,
    input logic             overflow_o
);

    logic resetting;
    logic count_up;
    logic count_down;


    logic init = 1'b0;
    always_ff @(posedge clk_i) init <= 1'b1;



    assume property (@(posedge clk_i) (!init) |-> !rst_ni);


    assign resetting = (clear_i || load_i);


    assign count_up = en_i && !down_i;
    assign count_down = en_i && down_i;


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (count_up && !resetting) |=> q_o == $past(q_o) + {{WIDTH-1{1'b0}}, 1'b1});


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (count_down && !resetting) |=> q_o == $past(q_o) - {{WIDTH-1{1'b0}}, 1'b1});


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        clear_i |=> q_o == '0);


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (load_i && !clear_i) |=> q_o == $past(d_i));



    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (($past(q_o) > q_o) && $past(count_up) && $past(!resetting) && $past(!overflow_o))
        |-> (overflow_o));
    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (($past(q_o) < q_o) && $past(count_down) && $past(!resetting) && $past(!overflow_o))
        |-> (overflow_o));


    if (STICKY_OVERFLOW == 1'b1) begin
        assert property(@(posedge clk_i)
            disable iff (!rst_ni)
            (overflow_o && !resetting |=> overflow_o));
    end


    cover property (@(posedge clk_i)
        overflow_o == 1'b1);
    cover property (@(posedge clk_i)
        clear_i == 1'b1);
    cover property (@(posedge clk_i)
        load_i == 1'b1);

endmodule
module counter_properties #(
    parameter int unsigned WIDTH = 4,
    parameter bit STICKY_OVERFLOW = 1'b0
)(
    input logic             clk_i,
    input logic             rst_ni,
    input logic             clear_i,
    input logic             en_i,
    input logic             load_i,
    input logic             down_i,
    input logic [WIDTH-1:0] d_i,
    input logic [WIDTH-1:0] q_o,
    input logic             overflow_o
);


    logic resetting;
    logic count_up;
    logic count_down;


    logic init = 1'b0;
    always_ff @(posedge clk_i) init <= 1'b1;



    assume property (@(posedge clk_i) (!init) |-> !rst_ni);


    assign resetting = (clear_i || load_i);


    assign count_up = en_i && !down_i;
    assign count_down = en_i && down_i;


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (count_up && !resetting) |=> q_o == $past(q_o) + {{WIDTH-1{1'b0}}, 1'b1});


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (count_down && !resetting) |=> q_o == $past(q_o) - {{WIDTH-1{1'b0}}, 1'b1});


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        clear_i |=> q_o == '0);


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (load_i && !clear_i) |=> q_o == $past(d_i));



    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (($past(q_o) > q_o) && $past(count_up) && $past(!resetting) && $past(!overflow_o))
        |-> (overflow_o));
    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (($past(q_o) < q_o) && $past(count_down) && $past(!resetting) && $past(!overflow_o))
        |-> (overflow_o));


    if (STICKY_OVERFLOW == 1'b1) begin
        assert property(@(posedge clk_i)
            disable iff (!rst_ni)
            (overflow_o && !resetting |=> overflow_o));
    end


    cover property (@(posedge clk_i)
        overflow_o == 1'b1);
    cover property (@(posedge clk_i)
        clear_i == 1'b1);
    cover property (@(posedge clk_i)
        load_i == 1'b1);

endmodule