data/full_repos/permissive/418284997/src/blocks/fifo.v
1: b'%Error: data/full_repos/permissive/418284997/src/blocks/fifo.v:4: Cannot find include file: bram_dual.v\n`include "bram_dual.v" \n         ^~~~~~~~~~~~~\n        ... Looked in:\n             data/full_repos/permissive/418284997/src/blocks,data/full_repos/permissive/418284997/bram_dual.v\n             data/full_repos/permissive/418284997/src/blocks,data/full_repos/permissive/418284997/bram_dual.v.v\n             data/full_repos/permissive/418284997/src/blocks,data/full_repos/permissive/418284997/bram_dual.v.sv\n             bram_dual.v\n             bram_dual.v.v\n             bram_dual.v.sv\n             obj_dir/bram_dual.v\n             obj_dir/bram_dual.v.v\n             obj_dir/bram_dual.v.sv\n%Error: Exiting due to 1 error(s)\n'
module fifo #(
    parameter memSize_p = 8,
    parameter dataWidth_p = 16
  )
  (
    input wire clk_i,
    input wire write_i,
    input wire read_i,
    input wire [(dataWidth_p - 1):0] data_i,

    output wire [(dataWidth_p - 1):0] data_o,
    output wire full_o,
    output wire empty_o
  );

  reg [(memSize_p - 1):0] index_read  = 0;
  reg [(memSize_p - 1):0] index_write = 0;



  assign full_o = index_read - index_write == 1;
  assign empty_o = index_read == index_write;

  always @(posedge clk_i) begin
    if (write_i) begin
      index_write <= index_write + 1'b1;


      if (index_write + 1'b1 == index_read)
        index_read <= index_read + 1'b1;
    end
    if (read_i) begin

      if (!empty_o)
        index_read <= index_read + 1'b1;

    end
  end

  bram_dual #(

    .memSize_p(memSize_p),
    .dataWidth_p(dataWidth_p)
  ) BRAM (
    .clk_i(clk_i),
    .write_i(write_i),
    .data_i(data_i),

    .waddr_i(index_write),
    .raddr_i(index_read),

    .data_o(data_o)
  );

  `ifdef FORMAL

    reg timeValid_f = 0;
    always @(posedge clk_i) timeValid_f <= 1;

    always @(posedge clk_i) begin

      if (full_o)
        assert(!empty_o);
      if (empty_o)
        assert(!full_o);
      

      if ($past(empty_o) && read_i && timeValid_f)
        assert($past(index_read) == index_read);
    end
    
  `endif

endmodule
module fifo #(
    parameter memSize_p = 8,
    parameter dataWidth_p = 16
  )
  (
    input wire clk_i,
    input wire write_i,
    input wire read_i,
    input wire [(dataWidth_p - 1):0] data_i,

    output wire [(dataWidth_p - 1):0] data_o,
    output wire full_o,
    output wire empty_o
  );


  reg [(memSize_p - 1):0] index_read  = 0;
  reg [(memSize_p - 1):0] index_write = 0;



  assign full_o = index_read - index_write == 1;
  assign empty_o = index_read == index_write;

  always @(posedge clk_i) begin
    if (write_i) begin
      index_write <= index_write + 1'b1;


      if (index_write + 1'b1 == index_read)
        index_read <= index_read + 1'b1;
    end
    if (read_i) begin

      if (!empty_o)
        index_read <= index_read + 1'b1;

    end
  end

  bram_dual #(

    .memSize_p(memSize_p),
    .dataWidth_p(dataWidth_p)
  ) BRAM (
    .clk_i(clk_i),
    .write_i(write_i),
    .data_i(data_i),

    .waddr_i(index_write),
    .raddr_i(index_read),

    .data_o(data_o)
  );

  `ifdef FORMAL

    reg timeValid_f = 0;
    always @(posedge clk_i) timeValid_f <= 1;

    always @(posedge clk_i) begin

      if (full_o)
        assert(!empty_o);
      if (empty_o)
        assert(!full_o);
      

      if ($past(empty_o) && read_i && timeValid_f)
        assert($past(index_read) == index_read);
    end
    
  `endif

endmodule