data/full_repos/permissive/418284997/src/rv32im/rv32im_memory.v
data/verilator_xmls/4afb6552-c188-4dad-8e83-b196e6cd27a2.xml
module rv32im_memory
  #(
    parameter XLEN = 32
  )
  (
    input wire clk_i,

    input wire clear_i,
    input wire data_ready_i,

    input wire [XLEN-1:0] data_i,
    output reg [XLEN-1:0] data_o,
    input wire [XLEN-1:0] addr_i,
    input wire [1:0] word_size_i,
    input wire write_i,
    output reg busy_o,

    output reg err_o,


    input wire [XLEN-1:0] master_dat_i,
    output reg [XLEN-1:0] master_dat_o,
    input wire ack_i,
    output reg [XLEN-1:2] adr_o,

    output wire cyc_o,

    input wire err_i,
    output reg [3:0] sel_o,
    output reg stb_o,
    output reg we_o
  );


  assign cyc_o = stb_o;





  reg [3:0] sel;
  always @(*) begin
    case (word_size_i)
      default: sel = 4'b0001 << addr_i[1:0];
      2'b01: sel = addr_i[1] ? 4'b1100 : 4'b0011;
      2'b10: sel = 4'b1111;
    endcase
  end

  always @(posedge clk_i) begin
    if (clear_i) begin
      stb_o <= 1'b0;
      sel_o <= 0;
      we_o <= 1'b0;
      busy_o <= 1'b0;
      err_o <= 1'b0;
    end else if (data_ready_i & ~stb_o) begin
      busy_o <= 1'b1;
      adr_o <= addr_i[XLEN-1:2];
      sel_o <= sel;
      stb_o <= 1'b1;
      master_dat_o <= data_i;
      we_o <= write_i;
    end else if (stb_o & err_i) begin

      stb_o <= 1'b0;
      sel_o <= 0;
      we_o <= 1'b0;
      busy_o <= 1'b0;
      err_o <= 1'b1;
    end else if (stb_o & ack_i) begin

      stb_o <= 1'b0;
      busy_o <= 1'b0;
      we_o <= 1'b0;
      data_o <= master_dat_i;
    end 
  end

  `ifdef FORMAL
    reg  timeValid_f;
    initial timeValid_f = 0;
    always @(posedge clk_i) 
      timeValid_f <= 1;

    always @(*)
      assume(clear_i == ~timeValid_f);

    always @(posedge clk_i) begin

      if (timeValid_f & $past(timeValid_f) & $past(clear_i)) begin
        assert(stb_o == 1'b0);
        assert(sel_o == 0);
        assert(we_o == 1'b0);
        assert(busy_o == 1'b0);
        assert(err_o == 1'b0);
      end


      if (timeValid_f & $past(timeValid_f) & $past(stb_o & ack_i & ~err_i)) begin
        assert(stb_o == 0);
        assert(busy_o == 0);
        assert(we_o == 0);
        assert(data_o == $past(master_dat_i));
      end



      if (timeValid_f & $past(timeValid_f) & $past(stb_o & err_i)) begin
        assert(stb_o == 0);
        assert(busy_o == 0);
        assert(we_o == 0);


        assert(err_o == 1'b1);
      end


      if (timeValid_f & $past(timeValid_f) & $past(~stb_o & data_ready_i)) begin
        if ($past(word_size_i) == 2'b01) begin


          if ($past(addr_i[1:0]) == 0 || $past(addr_i[1:0]) == 1)
            assert(sel_o == 4'b0011);
          else
            assert(sel_o == 4'b1100);
        end else if ($past(word_size_i) == 2'b10) begin
          assert(sel_o == 4'b1111);
        end else begin
          if ($past(addr_i[1:0]) == 0)
            assert(sel_o == 4'b0001);
          else if ($past(addr_i[1:0]) == 1)
            assert(sel_o == 4'b0010);
          else if ($past(addr_i[1:0]) == 2)
            assert(sel_o == 4'b0100);
          else if ($past(addr_i[1:0]) == 3)
            assert(sel_o == 4'b1000);
        end
      end

    end

  `endif


endmodule
module rv32im_memory
  #(
    parameter XLEN = 32
  )
  (
    input wire clk_i,

    input wire clear_i,
    input wire data_ready_i,

    input wire [XLEN-1:0] data_i,
    output reg [XLEN-1:0] data_o,
    input wire [XLEN-1:0] addr_i,
    input wire [1:0] word_size_i,
    input wire write_i,
    output reg busy_o,

    output reg err_o,


    input wire [XLEN-1:0] master_dat_i,
    output reg [XLEN-1:0] master_dat_o,
    input wire ack_i,
    output reg [XLEN-1:2] adr_o,

    output wire cyc_o,

    input wire err_i,
    output reg [3:0] sel_o,
    output reg stb_o,
    output reg we_o
  );



  assign cyc_o = stb_o;





  reg [3:0] sel;
  always @(*) begin
    case (word_size_i)
      default: sel = 4'b0001 << addr_i[1:0];
      2'b01: sel = addr_i[1] ? 4'b1100 : 4'b0011;
      2'b10: sel = 4'b1111;
    endcase
  end

  always @(posedge clk_i) begin
    if (clear_i) begin
      stb_o <= 1'b0;
      sel_o <= 0;
      we_o <= 1'b0;
      busy_o <= 1'b0;
      err_o <= 1'b0;
    end else if (data_ready_i & ~stb_o) begin
      busy_o <= 1'b1;
      adr_o <= addr_i[XLEN-1:2];
      sel_o <= sel;
      stb_o <= 1'b1;
      master_dat_o <= data_i;
      we_o <= write_i;
    end else if (stb_o & err_i) begin

      stb_o <= 1'b0;
      sel_o <= 0;
      we_o <= 1'b0;
      busy_o <= 1'b0;
      err_o <= 1'b1;
    end else if (stb_o & ack_i) begin

      stb_o <= 1'b0;
      busy_o <= 1'b0;
      we_o <= 1'b0;
      data_o <= master_dat_i;
    end 
  end

  `ifdef FORMAL
    reg  timeValid_f;
    initial timeValid_f = 0;
    always @(posedge clk_i) 
      timeValid_f <= 1;

    always @(*)
      assume(clear_i == ~timeValid_f);

    always @(posedge clk_i) begin

      if (timeValid_f & $past(timeValid_f) & $past(clear_i)) begin
        assert(stb_o == 1'b0);
        assert(sel_o == 0);
        assert(we_o == 1'b0);
        assert(busy_o == 1'b0);
        assert(err_o == 1'b0);
      end


      if (timeValid_f & $past(timeValid_f) & $past(stb_o & ack_i & ~err_i)) begin
        assert(stb_o == 0);
        assert(busy_o == 0);
        assert(we_o == 0);
        assert(data_o == $past(master_dat_i));
      end



      if (timeValid_f & $past(timeValid_f) & $past(stb_o & err_i)) begin
        assert(stb_o == 0);
        assert(busy_o == 0);
        assert(we_o == 0);


        assert(err_o == 1'b1);
      end


      if (timeValid_f & $past(timeValid_f) & $past(~stb_o & data_ready_i)) begin
        if ($past(word_size_i) == 2'b01) begin


          if ($past(addr_i[1:0]) == 0 || $past(addr_i[1:0]) == 1)
            assert(sel_o == 4'b0011);
          else
            assert(sel_o == 4'b1100);
        end else if ($past(word_size_i) == 2'b10) begin
          assert(sel_o == 4'b1111);
        end else begin
          if ($past(addr_i[1:0]) == 0)
            assert(sel_o == 4'b0001);
          else if ($past(addr_i[1:0]) == 1)
            assert(sel_o == 4'b0010);
          else if ($past(addr_i[1:0]) == 2)
            assert(sel_o == 4'b0100);
          else if ($past(addr_i[1:0]) == 3)
            assert(sel_o == 4'b1000);
        end
      end

    end

  `endif


endmodule