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

    STR_KER_WIDTH   = 64,

    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 [CFG_DWIDTH-1:0]                    cfg_data,
    input  wire [CFG_AWIDTH-1:0]                    cfg_addr,
    input  wire                                     cfg_valid,

    input  wire [STR_KER_WIDTH-1:0]                 str_ker_bus,
    input  wire                                     str_ker_val,
    output wire                                     str_ker_rdy,

    output wire [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   bias_bus,
    output wire [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   kernel_bus,
    input  wire                                     kernel_rdy
);




`include "cfg_parameters.vh"




    reg  [MEM_AWIDTH-1:0]                   wr_cfg_end;
    reg                                     wr_cfg_set;
    wire [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]  wr_data;
    wire                                    wr_data_val;
    wire                                    wr_data_rdy;

    reg  [MEM_AWIDTH-1:0]                   rd_cfg_start;
    reg  [MEM_AWIDTH-1:0]                   rd_cfg_end;
    reg                                     rd_cfg_set;





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

        if (cfg_valid & (cfg_addr == CFG_KER_WR)) begin
            wr_cfg_end  <= cfg_data[0 +: MEM_AWIDTH];
            wr_cfg_set  <= 1'b1;
        end
    end


    always @(posedge clk) begin
        rd_cfg_start    <= 'b0;
        rd_cfg_end      <= 'b0;
        rd_cfg_set      <= 1'b0;

        if (cfg_valid & (cfg_addr == CFG_KER_RD)) begin
            rd_cfg_start    <= cfg_data[0            +: MEM_AWIDTH];
            rd_cfg_end      <= cfg_data[CFG_DWIDTH/2 +: MEM_AWIDTH];
            rd_cfg_set      <= 1'b1;
        end
    end



    str_gbox #(
        .DATA_UP_WIDTH  (STR_KER_WIDTH),
        .DATA_DN_WIDTH  (GROUP_NB*KER_WIDTH*DEPTH_NB))
    str_gbox_ (
        .clk        (clk),
        .rst        (rst),

        .up_data    (str_ker_bus),
        .up_last    (1'b0),
        .up_val     (str_ker_val),
        .up_rdy     (str_ker_rdy),

        .dn_data    (wr_data),
        .dn_last    (),
        .dn_val     (wr_data_val),
        .dn_rdy     (wr_data_rdy)
    );



    kernel_mem #(
        .GROUP_NB   (GROUP_NB),
        .KER_WIDTH  (KER_WIDTH),
        .DEPTH_NB   (DEPTH_NB),

        .MEM_AWIDTH (MEM_AWIDTH),
        .MEM_DEPTH  (MEM_DEPTH))
    kernel_mem_ (
        .clk            (clk),
        .rst            (rst),


        .wr_cfg_end     (wr_cfg_end),
        .wr_cfg_set     (wr_cfg_set),
        .wr_data        (wr_data),
        .wr_data_val    (wr_data_val),
        .wr_data_rdy    (wr_data_rdy),

        .rd_cfg_start   (rd_cfg_start),
        .rd_cfg_end     (rd_cfg_end),
        .rd_cfg_set     (rd_cfg_set),
        .rd_bias        (bias_bus),
        .rd_data        (kernel_bus),
        .rd_data_rdy    (kernel_rdy)
    );



`ifdef FORMAL

`ifdef KERNEL
`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;




    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(str_ker_val && ~str_ker_rdy)) begin
            `ASSUME($stable(str_ker_bus));
        end



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



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



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

    STR_KER_WIDTH   = 64,

    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 [CFG_DWIDTH-1:0]                    cfg_data,
    input  wire [CFG_AWIDTH-1:0]                    cfg_addr,
    input  wire                                     cfg_valid,

    input  wire [STR_KER_WIDTH-1:0]                 str_ker_bus,
    input  wire                                     str_ker_val,
    output wire                                     str_ker_rdy,

    output wire [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   bias_bus,
    output wire [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]   kernel_bus,
    input  wire                                     kernel_rdy
);





`include "cfg_parameters.vh"




    reg  [MEM_AWIDTH-1:0]                   wr_cfg_end;
    reg                                     wr_cfg_set;
    wire [GROUP_NB*KER_WIDTH*DEPTH_NB-1:0]  wr_data;
    wire                                    wr_data_val;
    wire                                    wr_data_rdy;

    reg  [MEM_AWIDTH-1:0]                   rd_cfg_start;
    reg  [MEM_AWIDTH-1:0]                   rd_cfg_end;
    reg                                     rd_cfg_set;





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

        if (cfg_valid & (cfg_addr == CFG_KER_WR)) begin
            wr_cfg_end  <= cfg_data[0 +: MEM_AWIDTH];
            wr_cfg_set  <= 1'b1;
        end
    end


    always @(posedge clk) begin
        rd_cfg_start    <= 'b0;
        rd_cfg_end      <= 'b0;
        rd_cfg_set      <= 1'b0;

        if (cfg_valid & (cfg_addr == CFG_KER_RD)) begin
            rd_cfg_start    <= cfg_data[0            +: MEM_AWIDTH];
            rd_cfg_end      <= cfg_data[CFG_DWIDTH/2 +: MEM_AWIDTH];
            rd_cfg_set      <= 1'b1;
        end
    end



    str_gbox #(
        .DATA_UP_WIDTH  (STR_KER_WIDTH),
        .DATA_DN_WIDTH  (GROUP_NB*KER_WIDTH*DEPTH_NB))
    str_gbox_ (
        .clk        (clk),
        .rst        (rst),

        .up_data    (str_ker_bus),
        .up_last    (1'b0),
        .up_val     (str_ker_val),
        .up_rdy     (str_ker_rdy),

        .dn_data    (wr_data),
        .dn_last    (),
        .dn_val     (wr_data_val),
        .dn_rdy     (wr_data_rdy)
    );



    kernel_mem #(
        .GROUP_NB   (GROUP_NB),
        .KER_WIDTH  (KER_WIDTH),
        .DEPTH_NB   (DEPTH_NB),

        .MEM_AWIDTH (MEM_AWIDTH),
        .MEM_DEPTH  (MEM_DEPTH))
    kernel_mem_ (
        .clk            (clk),
        .rst            (rst),


        .wr_cfg_end     (wr_cfg_end),
        .wr_cfg_set     (wr_cfg_set),
        .wr_data        (wr_data),
        .wr_data_val    (wr_data_val),
        .wr_data_rdy    (wr_data_rdy),

        .rd_cfg_start   (rd_cfg_start),
        .rd_cfg_end     (rd_cfg_end),
        .rd_cfg_set     (rd_cfg_set),
        .rd_bias        (bias_bus),
        .rd_data        (kernel_bus),
        .rd_data_rdy    (kernel_rdy)
    );



`ifdef FORMAL

`ifdef KERNEL
`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;




    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(str_ker_val && ~str_ker_rdy)) begin
            `ASSUME($stable(str_ker_bus));
        end



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



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



`endif
endmodule