data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/fall_through_register_properties.sv
1: b"%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/fall_through_register_properties.sv:36: 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/fall_through_register_properties.sv:44: Unsupported or unknown PLI call: $stable\n        (valid_i && !ready_o |=> valid_i && $stable(data_i)));  \n                                            ^~~~~~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/fall_through_register_properties.sv:49: syntax error, unexpected |=>\n        (valid_o && !ready_i |=> valid_o && $stable(data_o)));  \n                             ^~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/fall_through_register_properties.sv:49: Unsupported or unknown PLI call: $stable\n        (valid_o && !ready_i |=> valid_o && $stable(data_o)));  \n                                            ^~~~~~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/fall_through_register_properties.sv:54: syntax error, unexpected |->\n        ((valid_i && ready_o) && ready_i |-> valid_o && (data_i == data_o)));\n                                         ^~~\n%Error: data/full_repos/permissive/489147019/Testcases/mempool/rtl/common_cells/formal/fall_through_register_properties.sv:77: syntax error, unexpected ##, expecting ')'\n        !ready_i ##5 ready_i);\n                 ^~\n%Error: Exiting due to 6 error(s)\n"
module fall_through_register_properties #(
    parameter type T = logic
)(
    input  logic    clk_i,
    input  logic    rst_ni,
    input  logic    clr_i,
    input  logic    testmode_i,

    input  logic    valid_i,
    input  logic    ready_o,
    input  T        data_i,

    input  logic    valid_o,
    input  logic    ready_i,
    input  T        data_o
);
    int    stalls = 0;

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



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


    assume property (@(posedge clk_i) clr_i == 1'b0);


    assume property (@(posedge clk_i)
        disable iff (!rst_ni)
        (valid_i && !ready_o |=> valid_i && $stable(data_i)));


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (valid_o && !ready_i |=> valid_o && $stable(data_o)));


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        ((valid_i && ready_o) && ready_i |-> valid_o && (data_i == data_o)));


    always_ff @(posedge clk_i or negedge rst_ni) begin

        if (!rst_ni || !valid_i || ready_o) begin
            stalls <= 0;
        end else if (valid_i && !ready_o) begin
            stalls <= stalls + 1;
        end
    end






    cover property (@(posedge clk_i)
        (valid_i && ready_o));
    cover property (@(posedge clk_i)
        (valid_o && ready_i));

    cover property (@(posedge clk_i)
        !ready_i ##5 ready_i);
    cover property (@(posedge clk_i)
        stalls > 10);

endmodule
module fall_through_register_properties #(
    parameter type T = logic
)(
    input  logic    clk_i,
    input  logic    rst_ni,
    input  logic    clr_i,
    input  logic    testmode_i,

    input  logic    valid_i,
    input  logic    ready_o,
    input  T        data_i,

    input  logic    valid_o,
    input  logic    ready_i,
    input  T        data_o
);

    int    stalls = 0;

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



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


    assume property (@(posedge clk_i) clr_i == 1'b0);


    assume property (@(posedge clk_i)
        disable iff (!rst_ni)
        (valid_i && !ready_o |=> valid_i && $stable(data_i)));


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        (valid_o && !ready_i |=> valid_o && $stable(data_o)));


    assert property (@(posedge clk_i)
        disable iff (!rst_ni)
        ((valid_i && ready_o) && ready_i |-> valid_o && (data_i == data_o)));


    always_ff @(posedge clk_i or negedge rst_ni) begin

        if (!rst_ni || !valid_i || ready_o) begin
            stalls <= 0;
        end else if (valid_i && !ready_o) begin
            stalls <= stalls + 1;
        end
    end






    cover property (@(posedge clk_i)
        (valid_i && ready_o));
    cover property (@(posedge clk_i)
        (valid_o && ready_i));

    cover property (@(posedge clk_i)
        !ready_i ##5 ready_i);
    cover property (@(posedge clk_i)
        stalls > 10);

endmodule