data/full_repos/permissive/418284997/src/blocks/bram_mask.v
1: b"%Error: data/full_repos/permissive/418284997/src/blocks/bram_mask.v:27: Cannot find file containing module: 'bitwise_mux'\n  bitwise_mux #(\n  ^~~~~~~~~~~\n        ... Looked in:\n             data/full_repos/permissive/418284997/src/blocks,data/full_repos/permissive/418284997/bitwise_mux\n             data/full_repos/permissive/418284997/src/blocks,data/full_repos/permissive/418284997/bitwise_mux.v\n             data/full_repos/permissive/418284997/src/blocks,data/full_repos/permissive/418284997/bitwise_mux.sv\n             bitwise_mux\n             bitwise_mux.v\n             bitwise_mux.sv\n             obj_dir/bitwise_mux\n             obj_dir/bitwise_mux.v\n             obj_dir/bitwise_mux.sv\n%Error: Exiting due to 1 error(s)\n"
module bram_mask
  #(
    parameter MEMORY_SIZE = 8,
    parameter XLEN = 16
  )
  (
    input wire clk_i,
    input wire write_i,
    input wire [XLEN-1:0] data_i,
    input wire [XLEN-1:0] write_mask_i,

    input wire [MEMORY_SIZE-1:0]  addr_i,

    output wire [XLEN-1:0] data_o
  );

  reg [XLEN-1:0] memory [2**MEMORY_SIZE-1:0];

  wire [XLEN-1:0] data_mux;

  bitwise_mux #(
    .LENGTH(XLEN)
  ) BITWISE_MUX (
    .data1_i(data_i),
    .data2_i(data_o),
    .select(write_mask_i),
    .data_o(data_mux)
  );

  always @(posedge clk_i) begin
    if (write_i) memory[addr_i] <= data_mux;
  end

  assign data_o = memory[addr_i];

  `ifdef FORMAL

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

    always @(posedge clk_i) begin

      if (timeValid_f && $past(write_i)) begin
        assert(memory[$past(waddr_i)] == $past(data_i));
      end





    end
    
  `endif

endmodule
module bram_mask
  #(
    parameter MEMORY_SIZE = 8,
    parameter XLEN = 16
  )
  (
    input wire clk_i,
    input wire write_i,
    input wire [XLEN-1:0] data_i,
    input wire [XLEN-1:0] write_mask_i,

    input wire [MEMORY_SIZE-1:0]  addr_i,

    output wire [XLEN-1:0] data_o
  );


  reg [XLEN-1:0] memory [2**MEMORY_SIZE-1:0];

  wire [XLEN-1:0] data_mux;

  bitwise_mux #(
    .LENGTH(XLEN)
  ) BITWISE_MUX (
    .data1_i(data_i),
    .data2_i(data_o),
    .select(write_mask_i),
    .data_o(data_mux)
  );

  always @(posedge clk_i) begin
    if (write_i) memory[addr_i] <= data_mux;
  end

  assign data_o = memory[addr_i];

  `ifdef FORMAL

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

    always @(posedge clk_i) begin

      if (timeValid_f && $past(write_i)) begin
        assert(memory[$past(waddr_i)] == $past(data_i));
      end





    end
    
  `endif

endmodule