Skip to content
Snippets Groups Projects
verifier.sv 2.41 KiB
module verifier #(
  parameter int unsigned NR_ENTRIES = 8,
  parameter int unsigned NR_COMMIT_PORTS = 2
) (
  input logic                       clk_i,
  input logic                       rst_ni,
  input logic                       flush_i,

  // I$
  input logic                       icache_miss_i,

  // Frontend
  input logic                       if_has_mem_access_i,

  // ID
  input logic                       id_has_mem_access_i,

  // IS
  input logic                       is_has_mem_access_i,

  // LSU
  input logic                       no_st_pending_commit_i,

  // CO
  input                             ariane_pkg::scoreboard_entry_t [NR_COMMIT_PORTS-1:0] commit_instr_i,
  input logic [NR_COMMIT_PORTS-1:0] commit_ack_i,

  output logic                      should_lock_icache_o
);

  localparam int unsigned           BITS_ENTRIES = $clog2(NR_ENTRIES);

  // Bus accesses (I$ misses and memory instructions in the pipeline)
  logic                             has_mem_access;
  assign has_mem_access = if_has_mem_access_i | id_has_mem_access_i | is_has_mem_access_i | (~no_st_pending_commit_i);
  assign should_lock_icache_o = has_mem_access & icache_miss_i;

  // CO
  logic [NR_COMMIT_PORTS-1:0][BITS_ENTRIES-1:0]          commit_id_n, commit_id_q;
  logic [NR_COMMIT_PORTS-1:0]       commit_correct;
  logic [BITS_ENTRIES-1:0]          commit_nr;

  popcount #(
    .INPUT_WIDTH (NR_COMMIT_PORTS)
  ) (
    .data_i (commit_ack_i),
    .popcount_o (commit_nr)
  );

  assign commit_id_n[0] = (flush_i) ? '0 : commit_id_q[0] + commit_nr;

  for (genvar i = 1; i < NR_COMMIT_PORTS; i++) begin
    assign commit_id_n[i] = (flush_i) ? '0 : commit_id_n[0] + i;
  end

  for (genvar i = 0; i < NR_COMMIT_PORTS; i++) begin
    assign commit_correct[i] = !(commit_instr_i[i].valid) ||
      (commit_instr_i[i].valid & commit_instr_i[i].trans_id == commit_id_q[i]);
  end

  always_ff @(posedge clk_i or negedge rst_ni) begin : regs
    if (!rst_ni) begin
      commit_id_q <= '0;
    end else begin
      commit_id_q <= commit_id_n;
    end
  end

  //pragma translate off
  `ifndef VERILATOR
  initial begin
    assert (NR_ENTRIES == 2**BITS_ENTRIES) else $fatal ("NR_ENTRIES is not a power of 2");
  end

  for (genvar i = 0; i < NR_COMMIT_PORTS; i++) begin
    assert property (
      @(posedge clk_i) disable iff (!rst_ni) commit_ack_i[i] |-> commit_correct[i])
      else $warning (1,"Invalid commit");
  end
  `endif
  //pragma translate on

endmodule