data/full_repos/permissive/153960117/hdl/image_write.v
1: b'%Error: data/full_repos/permissive/153960117/hdl/image_write.v:61: Cannot find include file: cfg_parameters.vh\n`include "cfg_parameters.vh" \n         ^~~~~~~~~~~~~~~~~~~\n        ... Looked in:\n             data/full_repos/permissive/153960117/hdl,data/full_repos/permissive/153960117/cfg_parameters.vh\n             data/full_repos/permissive/153960117/hdl,data/full_repos/permissive/153960117/cfg_parameters.vh.v\n             data/full_repos/permissive/153960117/hdl,data/full_repos/permissive/153960117/cfg_parameters.vh.sv\n             cfg_parameters.vh\n             cfg_parameters.vh.v\n             cfg_parameters.vh.sv\n             obj_dir/cfg_parameters.vh\n             obj_dir/cfg_parameters.vh.v\n             obj_dir/cfg_parameters.vh.sv\n%Error: Exiting due to 1 error(s)\n'
module image_write
  #(parameter
    CFG_DWIDTH  = 32,
    CFG_AWIDTH  = 5,

    DEPTH_NB    = 16,
    IMG_WIDTH   = 16,

    MEM_AWIDTH  = 16)
   (input  wire                             clk,
    input  wire                             rst,

    input  wire [CFG_DWIDTH-1:0]            cfg_data,
    input  wire [CFG_AWIDTH-1:0]            cfg_addr,
    input  wire                             cfg_valid,


    input  wire                             next,
    output reg                              next_rdy,

    input  wire [IMG_WIDTH*DEPTH_NB-1:0]    str_img_bus,
    input  wire                             str_img_val,
    output reg                              str_img_rdy,

    output wire                             wr_val,
    output wire [MEM_AWIDTH-1:0]            wr_addr,
    output wire [IMG_WIDTH*DEPTH_NB-1:0]    wr_data
);




`include "cfg_parameters.vh"




    reg  [31:0]                     cfg_img_w;
    reg  [15:0]                     cfg_img_h;

    reg  [15:0]                     cfg_start;
    reg  [15:0]                     cfg_step_p;
    reg  [15:0]                     cfg_step_r;

    reg  [31:0]                     img_w_max;
    reg  [31:0]                     img_h_max;
    reg  [31:0]                     start;
    reg  [31:0]                     step_p_max;
    reg  [31:0]                     step_p;
    reg  [31:0]                     step_r;

    reg                             rst_complete;
    reg                             next_1p;
    wire                            done;

    reg  [31:0]                     addr_w;
    reg  [31:0]                     addr_h;
    reg  [31:0]                     addr_d;

    wire                            addr_w_last;
    wire                            addr_h_last;
    wire                            addr_d_last;

    reg  [31:0]                     addr_w_1p;
    reg  [31:0]                     addr_h_1p;
    reg  [31:0]                     addr_d_1p;

    reg  [31:0]                     addr_w_2p;
    reg  [31:0]                     addr_h_2p;
    reg  [31:0]                     addr_d_2p;

    reg  [31:0]                     addr_h_3p;
    reg  [31:0]                     addr_dw_3p;

    reg  [31:0]                     addr_h_4p;
    reg  [31:0]                     addr_dw_4p;

    reg  [31:0]                     addr_5p;

    reg                             addr_val_1p;
    reg                             addr_val_2p;
    reg                             addr_val_3p;
    reg                             addr_val_4p;
    reg                             addr_val_5p;

    reg                             addr_last_1p;
    reg                             addr_last_2p;
    reg                             addr_last_3p;
    reg                             addr_last_4p;
    reg                             addr_last_5p;
    wire                            wr_last;

    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_1p;
    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_2p;
    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_3p;
    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_4p;
    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_5p;





    always @(posedge clk)
        if (cfg_valid & (cfg_addr == CFG_IW_IMG_W)) begin
            cfg_img_w   <= cfg_data;
        end


    always @(posedge clk)
        if (cfg_valid & (cfg_addr == CFG_IW_START)) begin
            cfg_start   <= cfg_data[31:16];
            cfg_img_h   <= cfg_data[15: 0];
        end


    always @(posedge clk)
        if (cfg_valid & (cfg_addr == CFG_IW_STEP)) begin
            cfg_step_p  <= cfg_data[31:16];
            cfg_step_r  <= cfg_data[15: 0];
        end



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

        if (next & next_rdy) begin
            next_1p     <= 1'b1;

            img_w_max   <= cfg_img_w;
            img_h_max   <= cfg_img_h;

            start       <= cfg_start;

            step_p_max  <= cfg_step_p;
            step_p      <= cfg_step_p + 'd1;
            step_r      <= cfg_step_r + 'd1;
        end
    end



    always @(posedge clk)
        if  (rst)   rst_complete <= 1'b1;
        else        rst_complete <= 1'b0;


    always @(posedge clk)
        if      (rst)                       next_rdy <= 1'b0;
        else if (rst_complete | wr_last)    next_rdy <= 1'b1;
        else if (next)                      next_rdy <= 1'b0;




    assign done = str_img_val & addr_w_last & addr_h_last & addr_d_last;


    always @(posedge clk)
        if      (rst)       str_img_rdy <= 1'b0;
        else if (next_1p)   str_img_rdy <= 1'b1;
        else if (done)      str_img_rdy <= 1'b0;





    assign addr_w_last  = (addr_w >= img_w_max);

    assign addr_h_last  = (addr_h >= img_h_max);

    assign addr_d_last  = (addr_d >= step_p_max);


    always @(posedge clk) begin
        if (rst) begin
            addr_w  <= 'b0;
            addr_h  <= 'b0;
            addr_d  <= 'b0;
        end
        else if (str_img_val & str_img_rdy) begin

            addr_w <= addr_w + 'd1;
            if (addr_w_last) begin

                addr_w  <= 'b0;
                addr_h  <= addr_h + 'd1;
                if (addr_h_last) begin

                    addr_h  <= 'b0;
                    addr_d  <= addr_d + 'd1;
                    if (addr_d_last) begin

                        addr_d <= 'b0;
                    end
                end
            end
        end
    end



    always @(posedge clk) begin
        addr_w_1p <= addr_w * step_p;
        addr_w_2p <= addr_w_1p;

        addr_h_1p <= addr_h * step_p;
        addr_h_2p <= addr_h_1p;

        addr_d_1p <= addr_d + start;
        addr_d_2p <= addr_d_1p;
    end


    always @(posedge clk) begin
        addr_h_3p <= addr_h_2p * step_r;
        addr_h_4p <= addr_h_3p;

        addr_dw_3p  <= addr_d_2p + addr_w_2p;
        addr_dw_4p  <= addr_dw_3p;
    end


    always @(posedge clk) begin
        addr_5p <= addr_h_4p + addr_dw_4p;
    end


    always @(posedge clk) begin
        addr_val_1p <= str_img_val & str_img_rdy;
        addr_val_2p <= addr_val_1p;
        addr_val_3p <= addr_val_2p;
        addr_val_4p <= addr_val_3p;
        addr_val_5p <= addr_val_4p;
    end


    always @(posedge clk) begin
        addr_last_1p <= str_img_val & str_img_rdy & done;
        addr_last_2p <= addr_last_1p;
        addr_last_3p <= addr_last_2p;
        addr_last_4p <= addr_last_3p;
        addr_last_5p <= addr_last_4p;
    end


    always @(posedge clk) begin
        str_img_bus_1p <= str_img_bus;
        str_img_bus_2p <= str_img_bus_1p;
        str_img_bus_3p <= str_img_bus_2p;
        str_img_bus_4p <= str_img_bus_3p;
        str_img_bus_5p <= str_img_bus_4p;
    end


    assign wr_last  = addr_last_5p;

    assign wr_val   = addr_val_5p;

    assign wr_addr  = addr_5p[MEM_AWIDTH-1:0];

    assign wr_data  = str_img_bus_5p;



`ifdef FORMAL

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


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



    always @(posedge clk)
        past_exists <= 1'b1;



`ifdef IMAGE_WRITE


    always @(posedge clk) begin
        if (next_1p) begin
            `ASSUME ( (start + (img_w_max * step_p) + (img_h_max * step_p * step_r))
                    < (1<<MEM_AWIDTH)
                    );
        end
    end
`endif




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




    always @(*) begin
        assert(MEM_AWIDTH < 32);
    end








    always @(posedge clk)
        if (past_exists && $past(str_img_val && ~str_img_rdy)) begin
            `ASSUME($stable(str_img_bus));
        end



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



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



`ifdef IMAGE_WRITE






    reg  rst_done = 1'b0;
    always @(posedge clk)
        if (rst) rst_done <= 1'b1;


    always @(*)
        cover (rst_done && str_img_rdy && done
                && (img_w_max  > 0)
                && (img_h_max  > 0)
                && (step_p_max > 0)
                );
`endif


`endif
endmodule
module image_write
  #(parameter
    CFG_DWIDTH  = 32,
    CFG_AWIDTH  = 5,

    DEPTH_NB    = 16,
    IMG_WIDTH   = 16,

    MEM_AWIDTH  = 16)
   (input  wire                             clk,
    input  wire                             rst,

    input  wire [CFG_DWIDTH-1:0]            cfg_data,
    input  wire [CFG_AWIDTH-1:0]            cfg_addr,
    input  wire                             cfg_valid,


    input  wire                             next,
    output reg                              next_rdy,

    input  wire [IMG_WIDTH*DEPTH_NB-1:0]    str_img_bus,
    input  wire                             str_img_val,
    output reg                              str_img_rdy,

    output wire                             wr_val,
    output wire [MEM_AWIDTH-1:0]            wr_addr,
    output wire [IMG_WIDTH*DEPTH_NB-1:0]    wr_data
);





`include "cfg_parameters.vh"




    reg  [31:0]                     cfg_img_w;
    reg  [15:0]                     cfg_img_h;

    reg  [15:0]                     cfg_start;
    reg  [15:0]                     cfg_step_p;
    reg  [15:0]                     cfg_step_r;

    reg  [31:0]                     img_w_max;
    reg  [31:0]                     img_h_max;
    reg  [31:0]                     start;
    reg  [31:0]                     step_p_max;
    reg  [31:0]                     step_p;
    reg  [31:0]                     step_r;

    reg                             rst_complete;
    reg                             next_1p;
    wire                            done;

    reg  [31:0]                     addr_w;
    reg  [31:0]                     addr_h;
    reg  [31:0]                     addr_d;

    wire                            addr_w_last;
    wire                            addr_h_last;
    wire                            addr_d_last;

    reg  [31:0]                     addr_w_1p;
    reg  [31:0]                     addr_h_1p;
    reg  [31:0]                     addr_d_1p;

    reg  [31:0]                     addr_w_2p;
    reg  [31:0]                     addr_h_2p;
    reg  [31:0]                     addr_d_2p;

    reg  [31:0]                     addr_h_3p;
    reg  [31:0]                     addr_dw_3p;

    reg  [31:0]                     addr_h_4p;
    reg  [31:0]                     addr_dw_4p;

    reg  [31:0]                     addr_5p;

    reg                             addr_val_1p;
    reg                             addr_val_2p;
    reg                             addr_val_3p;
    reg                             addr_val_4p;
    reg                             addr_val_5p;

    reg                             addr_last_1p;
    reg                             addr_last_2p;
    reg                             addr_last_3p;
    reg                             addr_last_4p;
    reg                             addr_last_5p;
    wire                            wr_last;

    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_1p;
    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_2p;
    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_3p;
    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_4p;
    reg  [IMG_WIDTH*DEPTH_NB-1:0]   str_img_bus_5p;





    always @(posedge clk)
        if (cfg_valid & (cfg_addr == CFG_IW_IMG_W)) begin
            cfg_img_w   <= cfg_data;
        end


    always @(posedge clk)
        if (cfg_valid & (cfg_addr == CFG_IW_START)) begin
            cfg_start   <= cfg_data[31:16];
            cfg_img_h   <= cfg_data[15: 0];
        end


    always @(posedge clk)
        if (cfg_valid & (cfg_addr == CFG_IW_STEP)) begin
            cfg_step_p  <= cfg_data[31:16];
            cfg_step_r  <= cfg_data[15: 0];
        end



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

        if (next & next_rdy) begin
            next_1p     <= 1'b1;

            img_w_max   <= cfg_img_w;
            img_h_max   <= cfg_img_h;

            start       <= cfg_start;

            step_p_max  <= cfg_step_p;
            step_p      <= cfg_step_p + 'd1;
            step_r      <= cfg_step_r + 'd1;
        end
    end



    always @(posedge clk)
        if  (rst)   rst_complete <= 1'b1;
        else        rst_complete <= 1'b0;


    always @(posedge clk)
        if      (rst)                       next_rdy <= 1'b0;
        else if (rst_complete | wr_last)    next_rdy <= 1'b1;
        else if (next)                      next_rdy <= 1'b0;




    assign done = str_img_val & addr_w_last & addr_h_last & addr_d_last;


    always @(posedge clk)
        if      (rst)       str_img_rdy <= 1'b0;
        else if (next_1p)   str_img_rdy <= 1'b1;
        else if (done)      str_img_rdy <= 1'b0;





    assign addr_w_last  = (addr_w >= img_w_max);

    assign addr_h_last  = (addr_h >= img_h_max);

    assign addr_d_last  = (addr_d >= step_p_max);


    always @(posedge clk) begin
        if (rst) begin
            addr_w  <= 'b0;
            addr_h  <= 'b0;
            addr_d  <= 'b0;
        end
        else if (str_img_val & str_img_rdy) begin

            addr_w <= addr_w + 'd1;
            if (addr_w_last) begin

                addr_w  <= 'b0;
                addr_h  <= addr_h + 'd1;
                if (addr_h_last) begin

                    addr_h  <= 'b0;
                    addr_d  <= addr_d + 'd1;
                    if (addr_d_last) begin

                        addr_d <= 'b0;
                    end
                end
            end
        end
    end



    always @(posedge clk) begin
        addr_w_1p <= addr_w * step_p;
        addr_w_2p <= addr_w_1p;

        addr_h_1p <= addr_h * step_p;
        addr_h_2p <= addr_h_1p;

        addr_d_1p <= addr_d + start;
        addr_d_2p <= addr_d_1p;
    end


    always @(posedge clk) begin
        addr_h_3p <= addr_h_2p * step_r;
        addr_h_4p <= addr_h_3p;

        addr_dw_3p  <= addr_d_2p + addr_w_2p;
        addr_dw_4p  <= addr_dw_3p;
    end


    always @(posedge clk) begin
        addr_5p <= addr_h_4p + addr_dw_4p;
    end


    always @(posedge clk) begin
        addr_val_1p <= str_img_val & str_img_rdy;
        addr_val_2p <= addr_val_1p;
        addr_val_3p <= addr_val_2p;
        addr_val_4p <= addr_val_3p;
        addr_val_5p <= addr_val_4p;
    end


    always @(posedge clk) begin
        addr_last_1p <= str_img_val & str_img_rdy & done;
        addr_last_2p <= addr_last_1p;
        addr_last_3p <= addr_last_2p;
        addr_last_4p <= addr_last_3p;
        addr_last_5p <= addr_last_4p;
    end


    always @(posedge clk) begin
        str_img_bus_1p <= str_img_bus;
        str_img_bus_2p <= str_img_bus_1p;
        str_img_bus_3p <= str_img_bus_2p;
        str_img_bus_4p <= str_img_bus_3p;
        str_img_bus_5p <= str_img_bus_4p;
    end


    assign wr_last  = addr_last_5p;

    assign wr_val   = addr_val_5p;

    assign wr_addr  = addr_5p[MEM_AWIDTH-1:0];

    assign wr_data  = str_img_bus_5p;



`ifdef FORMAL

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


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



    always @(posedge clk)
        past_exists <= 1'b1;



`ifdef IMAGE_WRITE


    always @(posedge clk) begin
        if (next_1p) begin
            `ASSUME ( (start + (img_w_max * step_p) + (img_h_max * step_p * step_r))
                    < (1<<MEM_AWIDTH)
                    );
        end
    end
`endif




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




    always @(*) begin
        assert(MEM_AWIDTH < 32);
    end








    always @(posedge clk)
        if (past_exists && $past(str_img_val && ~str_img_rdy)) begin
            `ASSUME($stable(str_img_bus));
        end



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



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



`ifdef IMAGE_WRITE






    reg  rst_done = 1'b0;
    always @(posedge clk)
        if (rst) rst_done <= 1'b1;


    always @(*)
        cover (rst_done && str_img_rdy && done
                && (img_w_max  > 0)
                && (img_h_max  > 0)
                && (step_p_max > 0)
                );
`endif


`endif
endmodule