data/full_repos/permissive/153960117/hdl/kernel_mem.v
data/verilator_xmls/803ec05e-a24c-4ff2-9274-d5eb700fdfd1.xml
module kernel_mem
  #(parameter
    GROUP_NB    = 4,
    KER_WIDTH   = 16,
    DEPTH_NB    = 16,

    MEM_AWIDTH  = 16,
    MEM_DEPTH   = 1<<MEM_AWIDTH)
   (input  wire                                     clk,
    input  wire                                     rst,

    input  wire [MEM_AWIDTH-1:0]                    wr_cfg_end,
    input  wire                                     wr_cfg_set,

    input  wire [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   wr_data,
    input  wire                                     wr_data_val,
    output wire                                     wr_data_rdy,

    input  wire [MEM_AWIDTH-1:0]                    rd_cfg_start,
    input  wire [MEM_AWIDTH-1:0]                    rd_cfg_end,
    input  wire                                     rd_cfg_set,

    output reg  [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   rd_bias,
    output reg  [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   rd_data,
    input  wire                                     rd_data_rdy
);








    reg  [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]  mem [0:MEM_DEPTH-1];

    reg                     wr_ptr_wrap;
    reg  [MEM_AWIDTH-1:0]   wr_ptr;
    reg                     wr_end_wrap;
    reg  [MEM_AWIDTH-1:0]   wr_end;

    wire                    rd_data_pop;
    reg                     rd_data_1st;
    reg                     rd_data_2nd;
    reg  [MEM_AWIDTH-1:0]   rd_ptr;
    reg  [MEM_AWIDTH-1:0]   rd_start;
    reg  [MEM_AWIDTH-1:0]   rd_end;






    assign wr_data_rdy = ~((wr_ptr_wrap != wr_end_wrap) && (wr_ptr == wr_end));


    always @(posedge clk)
        if (rst) begin
            wr_end      <= 'b0;
            wr_end_wrap <= 1'b1;
        end
        else if (wr_cfg_set) begin
            wr_end <= wr_cfg_end;

            if (wr_end >= wr_cfg_end) begin




                wr_end_wrap <= ~wr_end_wrap;
            end
        end


    always @(posedge clk)
        if (rst) begin
            wr_ptr      <= 'b0;
            wr_ptr_wrap <= 1'b0;
        end
        else if (wr_data_val & wr_data_rdy) begin
            wr_ptr <= wr_ptr + {{MEM_AWIDTH-1{1'b0}}, 1'b1};

            if (wr_ptr == (MEM_DEPTH[MEM_AWIDTH-1:0]-1)) begin
                wr_ptr      <= 'b0;
                wr_ptr_wrap <= ~wr_ptr_wrap;
            end
        end


    always @(posedge clk)
        if (wr_data_val & wr_data_rdy) begin
            mem[wr_ptr] <= wr_data;
        end






    assign rd_data_pop = rd_data_1st | rd_data_2nd | rd_data_rdy;


    always @(posedge clk) begin
        rd_data_1st <= 1'b0;
        rd_data_2nd <= rd_data_1st;

        if (rd_cfg_set) begin
            rd_data_1st <= 1'b1;
            rd_data_2nd <= 1'b0;
        end
    end


    always @(posedge clk)
        if (rst) begin
            rd_start    <= 'b0;
            rd_end      <= 'b0;
        end
        else if (rd_cfg_set) begin
            rd_start    <= rd_cfg_start + 'b1;
            rd_end      <= rd_cfg_end;
        end


    always @(posedge clk)
        if (rd_cfg_set) begin
            rd_ptr <= rd_cfg_start;
        end
        else if (rd_data_pop) begin
            rd_ptr <= rd_ptr + {{MEM_AWIDTH-1{1'b0}}, 1'b1};

            if (rd_ptr >= (MEM_DEPTH[MEM_AWIDTH-1:0]-1)) begin
                rd_ptr <= 'b0;
            end

            if (rd_ptr == rd_end) begin

                rd_ptr <= rd_start;
            end
        end


    always @(posedge clk)
        if (rd_data_pop) begin
            rd_data <= mem[rd_ptr];
        end



    always @(posedge clk)
        if (rd_data_2nd) begin
            rd_bias <= rd_data;
        end


`ifdef FORMAL

`ifdef KERNEL_MEM
`define ASSUME assume
`else
`define ASSUME assert
`endif


    reg  past_exists;
    reg  past_exists_2;
    initial begin
        past_exists     = 1'b0;
        past_exists_2   = 1'b0;


        `ASSUME(wr_ptr      < MEM_DEPTH);
        `ASSUME(rd_ptr      < MEM_DEPTH);
        `ASSUME(wr_end      < MEM_DEPTH);
        `ASSUME(rd_end      < MEM_DEPTH);
        `ASSUME(rd_start    < MEM_DEPTH);
    end



    always @(posedge clk)
        {past_exists_2, past_exists} <= {past_exists, 1'b1};




    always @(*)
        assert(MEM_DEPTH <= (1<<MEM_AWIDTH));



    always @(*) begin
        assert(wr_ptr < MEM_DEPTH);
        assert(rd_ptr < MEM_DEPTH);
    end



    always @(*) begin
        `ASSUME(wr_cfg_end   < MEM_DEPTH);
        `ASSUME(rd_cfg_end   < MEM_DEPTH);
        `ASSUME(rd_cfg_start < MEM_DEPTH);





        `ASSUME(rd_cfg_set && (rd_cfg_start == rd_cfg_end));
    end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $past(wr_cfg_set) && ~wr_data_rdy) begin
            `ASSUME($past( ~wr_data_rdy));
        end



    always @(posedge clk)
        if (past_exists_2
        && $changed(rd_data)
        && $past( ~rd_cfg_set, 1)
        && $past( ~rd_cfg_set, 2)
        ) begin

            assert(rd_data_rdy);
        end



    always @(posedge clk)
        if (past_exists_2
        && $past( ~rd_cfg_set, 1)
        && $past( ~rd_cfg_set, 2)
        ) begin

            assert($stable(rd_bias));
        end








    always @(posedge clk)
        if (past_exists && $past(wr_data_val && ~wr_data_rdy)) begin
            `ASSUME($stable(wr_data));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(wr_data_val)) begin
            `ASSUME($past(wr_data_rdy));
        end



    always @(posedge clk)
        if (past_exists && ~rst && $past( ~rst) && $fell(wr_data_rdy)) begin
            assert($past(wr_data_val));
        end


`endif
endmodule
module kernel_mem
  #(parameter
    GROUP_NB    = 4,
    KER_WIDTH   = 16,
    DEPTH_NB    = 16,

    MEM_AWIDTH  = 16,
    MEM_DEPTH   = 1<<MEM_AWIDTH)
   (input  wire                                     clk,
    input  wire                                     rst,

    input  wire [MEM_AWIDTH-1:0]                    wr_cfg_end,
    input  wire                                     wr_cfg_set,

    input  wire [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   wr_data,
    input  wire                                     wr_data_val,
    output wire                                     wr_data_rdy,

    input  wire [MEM_AWIDTH-1:0]                    rd_cfg_start,
    input  wire [MEM_AWIDTH-1:0]                    rd_cfg_end,
    input  wire                                     rd_cfg_set,

    output reg  [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   rd_bias,
    output reg  [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   rd_data,
    input  wire                                     rd_data_rdy
);









    reg  [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]  mem [0:MEM_DEPTH-1];

    reg                     wr_ptr_wrap;
    reg  [MEM_AWIDTH-1:0]   wr_ptr;
    reg                     wr_end_wrap;
    reg  [MEM_AWIDTH-1:0]   wr_end;

    wire                    rd_data_pop;
    reg                     rd_data_1st;
    reg                     rd_data_2nd;
    reg  [MEM_AWIDTH-1:0]   rd_ptr;
    reg  [MEM_AWIDTH-1:0]   rd_start;
    reg  [MEM_AWIDTH-1:0]   rd_end;






    assign wr_data_rdy = ~((wr_ptr_wrap != wr_end_wrap) && (wr_ptr == wr_end));


    always @(posedge clk)
        if (rst) begin
            wr_end      <= 'b0;
            wr_end_wrap <= 1'b1;
        end
        else if (wr_cfg_set) begin
            wr_end <= wr_cfg_end;

            if (wr_end >= wr_cfg_end) begin




                wr_end_wrap <= ~wr_end_wrap;
            end
        end


    always @(posedge clk)
        if (rst) begin
            wr_ptr      <= 'b0;
            wr_ptr_wrap <= 1'b0;
        end
        else if (wr_data_val & wr_data_rdy) begin
            wr_ptr <= wr_ptr + {{MEM_AWIDTH-1{1'b0}}, 1'b1};

            if (wr_ptr == (MEM_DEPTH[MEM_AWIDTH-1:0]-1)) begin
                wr_ptr      <= 'b0;
                wr_ptr_wrap <= ~wr_ptr_wrap;
            end
        end


    always @(posedge clk)
        if (wr_data_val & wr_data_rdy) begin
            mem[wr_ptr] <= wr_data;
        end






    assign rd_data_pop = rd_data_1st | rd_data_2nd | rd_data_rdy;


    always @(posedge clk) begin
        rd_data_1st <= 1'b0;
        rd_data_2nd <= rd_data_1st;

        if (rd_cfg_set) begin
            rd_data_1st <= 1'b1;
            rd_data_2nd <= 1'b0;
        end
    end


    always @(posedge clk)
        if (rst) begin
            rd_start    <= 'b0;
            rd_end      <= 'b0;
        end
        else if (rd_cfg_set) begin
            rd_start    <= rd_cfg_start + 'b1;
            rd_end      <= rd_cfg_end;
        end


    always @(posedge clk)
        if (rd_cfg_set) begin
            rd_ptr <= rd_cfg_start;
        end
        else if (rd_data_pop) begin
            rd_ptr <= rd_ptr + {{MEM_AWIDTH-1{1'b0}}, 1'b1};

            if (rd_ptr >= (MEM_DEPTH[MEM_AWIDTH-1:0]-1)) begin
                rd_ptr <= 'b0;
            end

            if (rd_ptr == rd_end) begin

                rd_ptr <= rd_start;
            end
        end


    always @(posedge clk)
        if (rd_data_pop) begin
            rd_data <= mem[rd_ptr];
        end



    always @(posedge clk)
        if (rd_data_2nd) begin
            rd_bias <= rd_data;
        end


`ifdef FORMAL

`ifdef KERNEL_MEM
`define ASSUME assume
`else
`define ASSUME assert
`endif


    reg  past_exists;
    reg  past_exists_2;
    initial begin
        past_exists     = 1'b0;
        past_exists_2   = 1'b0;


        `ASSUME(wr_ptr      < MEM_DEPTH);
        `ASSUME(rd_ptr      < MEM_DEPTH);
        `ASSUME(wr_end      < MEM_DEPTH);
        `ASSUME(rd_end      < MEM_DEPTH);
        `ASSUME(rd_start    < MEM_DEPTH);
    end



    always @(posedge clk)
        {past_exists_2, past_exists} <= {past_exists, 1'b1};




    always @(*)
        assert(MEM_DEPTH <= (1<<MEM_AWIDTH));



    always @(*) begin
        assert(wr_ptr < MEM_DEPTH);
        assert(rd_ptr < MEM_DEPTH);
    end



    always @(*) begin
        `ASSUME(wr_cfg_end   < MEM_DEPTH);
        `ASSUME(rd_cfg_end   < MEM_DEPTH);
        `ASSUME(rd_cfg_start < MEM_DEPTH);





        `ASSUME(rd_cfg_set && (rd_cfg_start == rd_cfg_end));
    end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $past(wr_cfg_set) && ~wr_data_rdy) begin
            `ASSUME($past( ~wr_data_rdy));
        end



    always @(posedge clk)
        if (past_exists_2
        && $changed(rd_data)
        && $past( ~rd_cfg_set, 1)
        && $past( ~rd_cfg_set, 2)
        ) begin

            assert(rd_data_rdy);
        end



    always @(posedge clk)
        if (past_exists_2
        && $past( ~rd_cfg_set, 1)
        && $past( ~rd_cfg_set, 2)
        ) begin

            assert($stable(rd_bias));
        end








    always @(posedge clk)
        if (past_exists && $past(wr_data_val && ~wr_data_rdy)) begin
            `ASSUME($stable(wr_data));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(wr_data_val)) begin
            `ASSUME($past(wr_data_rdy));
        end



    always @(posedge clk)
        if (past_exists && ~rst && $past( ~rst) && $fell(wr_data_rdy)) begin
            assert($past(wr_data_val));
        end


`endif
endmodule