// Copyright lowRISC contributors.
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0

// FPV CSR read and write assertions auto-generated by `reggen` containing data structure
// Do Not Edit directly
// TODO: This automation does not support: shadow reg, has_d has_de not has_q (right now does not
// have internal storage if de=0)
<% from reggen import (gen_fpv)
%>\
<% from topgen import lib
%>\
<%def name="construct_classes(block)">\
% for b in block.blocks:
${construct_classes(b)}
% endfor

`include "prim_assert.sv"

// Block: ${block.name}
module ${block.name}_csr_assert_fpv import tlul_pkg::*; import ${block.name}_reg_pkg::*;
    import top_pkg::*;(
  input clk_i,
  input rst_ni,

  // tile link ports
  input tl_h2d_t h2d,
  input tl_d2h_t d2h,

  // reg and hw ports
  input ${block.name}_reg2hw_t reg2hw,
  input ${block.name}_hw2reg_t hw2reg
);

`ifndef VERILATOR
`ifndef SYNTHESIS

`ifdef UVM
  import uvm_pkg::*;
  % if block.hier_path:
  `define REGWEN_PATH dut.${block.hier_path}.u_reg
  % elif block.name == "flash_ctrl":
  `define REGWEN_PATH dut.u_flash_ctrl.u_reg
  % elif block.name == "sram_ctrl":
  `define REGWEN_PATH dut.u_sram_ctrl.u_reg
  % else:
  `define REGWEN_PATH dut.u_reg
  % endif
`else
  `define REGWEN_PATH u_reg
`endif

  bit disable_sva;

  // mask register to convert byte to bit
  logic [TL_DW-1:0] a_mask_bit;

  assign a_mask_bit[7:0]   = h2d.a_mask[0] ? '1 : '0;
  assign a_mask_bit[15:8]  = h2d.a_mask[1] ? '1 : '0;
  assign a_mask_bit[23:16] = h2d.a_mask[2] ? '1 : '0;
  assign a_mask_bit[31:24] = h2d.a_mask[3] ? '1 : '0;

<%
  addr_msb  = block.addr_width - 1
  reg_width = block.addr_width
%>\
  // normalized address only take the [${addr_msb}:2] address from the TLUL a_address
  bit [${addr_msb}:0] normalized_addr;
  assign normalized_addr = {h2d.a_address[${addr_msb}:2], 2'b0};

  // declare common read and write sequences
  sequence device_wr_S(logic [${addr_msb}:0] addr);
    normalized_addr == addr && h2d.a_opcode inside {PutFullData, PutPartialData} &&
        h2d.a_valid && h2d.d_ready && !d2h.d_valid;
  endsequence

  sequence device_rd_S(logic [${addr_msb}:0] addr);
    normalized_addr == addr && h2d.a_opcode inside {Get} && h2d.a_valid && h2d.d_ready &&
        !d2h.d_valid;
  endsequence

  // declare common read and write properties
  // for homog registers, we check by a reg; for non-homog regs, we check by field.
  // `mask` is used for checking by field. It masks out any act_data that are not within the field
  // `lsb` is used to check non-homog multi_reg. Because we are using a local copy `_fpv` variable
  // to store all the multi-reg within one basefield, we need to shift the `_fpv` value to the
  // correct bits, then compare with read/write exp_data.

  property wr_P(bit [${addr_msb}:0] addr, bit [TL_DW-1:0] act_data, bit regen,
                bit [TL_DW-1:0] mask, int lsb);
    logic [TL_DW-1:0] id, exp_data;
    (device_wr_S(addr) and regen, id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask) ##1
        first_match(##[0:$] d2h.d_valid && d2h.d_source == id) |->
        (d2h.d_error || (act_data << lsb) == exp_data);
  endproperty

  // this property is to check when regen is set to 0, the write data should not be updated
  property wr_regen_P(bit [${addr_msb}:0] addr, bit [TL_DW-1:0] act_data, bit regen,
                bit [TL_DW-1:0] mask, int lsb);
    logic [TL_DW-1:0] id, exp_data;
    (device_wr_S(addr) and !regen, id = h2d.a_source, exp_data = (act_data << lsb)) ##1
        first_match(##[0:$] d2h.d_valid && d2h.d_source == id) |->
        (d2h.d_error || (act_data << lsb) == exp_data);
  endproperty

  // external reg will use one clk cycle to update act_data from external
  property wr_ext_P(bit [${addr_msb}:0] addr, bit [TL_DW-1:0] act_data, bit regen,
                    bit [TL_DW-1:0] mask, int lsb);
    logic [TL_DW-1:0] id, exp_data;
    (device_wr_S(addr) and regen, id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask) ##1
        first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
        (d2h.d_error || ($past(act_data) << lsb) == exp_data);
  endproperty

  property wr_ext_regen_P(bit [${addr_msb}:0] addr, bit [TL_DW-1:0] act_data, bit regen,
                    bit [TL_DW-1:0] mask, int lsb);
    logic [TL_DW-1:0] id, exp_data;
    (device_wr_S(addr) and !regen, id = h2d.a_source, exp_data = (act_data << lsb)) ##1
        first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
        (d2h.d_error || ($past(act_data) << lsb) == exp_data);
  endproperty

  // W1C register, if write 1 external data will be cleared to 0;
  // if write 0, internal data won't change
  // TODO: add regen check for W1C regs
  property w1c_P(bit [${addr_msb}:0] addr, bit [TL_DW-1:0] act_data, bit regen,
                 bit [TL_DW-1:0] mask, int lsb);
    logic [TL_DW-1:0] id, exp_data;
    (device_wr_S(addr) and regen, id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask) ##1
        first_match(##[0:$] d2h.d_valid && d2h.d_source == id) |->
        (d2h.d_error || ((act_data << lsb) & exp_data) == 0);
  endproperty

  property w1c_ext_P(bit [${addr_msb}:0] addr, bit [TL_DW-1:0] act_data, bit regen,
                     bit [TL_DW-1:0] mask, int lsb);
    logic [TL_DW-1:0] id, exp_data;
    (device_wr_S(addr) and regen, id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask) ##1
        first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
        (d2h.d_error || ($past(act_data) << lsb) == exp_data);
  endproperty

  property rd_P(bit [${addr_msb}:0] addr, bit [TL_DW-1:0] act_data, bit [TL_DW-1:0] mask, int lsb);
    logic [TL_DW-1:0] id, exp_data;
    (device_rd_S(addr), id = h2d.a_source, exp_data = $past(act_data)) ##1
        first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
        (d2h.d_error || (d2h.d_data & mask) >> lsb == exp_data);
  endproperty

  property rd_ext_P(bit [${addr_msb}:0] addr, bit [TL_DW-1:0] act_data, bit [TL_DW-1:0] mask,
      int lsb);
    logic [TL_DW-1:0] id, exp_data;
    (device_rd_S(addr), id = h2d.a_source, exp_data = act_data) ##1
        first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
        (d2h.d_error || (d2h.d_data & mask) >> lsb == exp_data);
  endproperty

% for r in block.regs:
<%
  has_q  = r.get_n_bits(["q"]) > 0
  has_d  = r.get_n_bits(["d"]) > 0
  has_de = r.get_n_bits(["de"]) > 0
%>\
  % if not r.get_field_flat(0).shadowed:
  % if r.is_multi_reg():
<%
      mreg_name          = r.name
      mreg_width_list    = list()
      mreg_fpv_name_list = list()
      mreg_dut_path_list = list()
      mreg_has_q_list    = list()
      mreg_has_d_list    = list()
      mreg_has_de_list   = list()
      mreg_num_regs      = r.get_n_fields_flat()

      mreg_msb = -1
      mreg_lsb = 0
      i        = 0
%>\
   % if not r.ishomog:
     % for field in r.get_reg_flat(0).fields:
<%
  mreg_fpv_name_list.append(mreg_name + "_" + field.get_basename())
  mreg_dut_path_list.append(mreg_name + "[s]." + field.get_basename())
  mreg_width_list.append(field.msb - field.lsb + 1)
  mreg_has_q_list.append(field.get_n_bits(["q"]) > 0)
  mreg_has_d_list.append(field.get_n_bits(["d"]) > 0)
  mreg_has_de_list.append(field.get_n_bits(["de"]) > 0)
%>\
     % endfor
<%
  mreg_num_base_fields = len(mreg_fpv_name_list)
  mreg_num_regs        = mreg_num_regs / mreg_num_base_fields
%>\
   % else:
<%
  f = r.get_field_flat(0)
  mreg_num_base_fields = 1
  mreg_fpv_name_list.append(mreg_name)
  mreg_dut_path_list.append(mreg_name + "[s]")
  mreg_width_list.append(f.msb - f.lsb + 1)
  mreg_has_q_list.append(has_q)
  mreg_has_d_list.append(has_d)
  mreg_has_de_list.append(has_de)
%>\
   % endif

  // define local fpv variable for multi-reg
   % if r.get_n_bits(["q", "d"]):
     % for fpv_name in mreg_fpv_name_list:
${declare_fpv_var(fpv_name, int(mreg_width_list[loop.index] * mreg_num_regs - 1), loop.index)}\
     % endfor
  for (genvar s = 0; s < ${int(mreg_num_regs)}; s++) begin : gen_${mreg_name}_q
     % for fpv_name in mreg_fpv_name_list:
${assign_fpv_var(fpv_name, mreg_dut_path_list[loop.index], int(mreg_width_list[loop.index]), loop.index)}\
     % endfor
  end
   % endif
  % endif

  % for reg_flat in r.get_regs_flat():
<%
  reg_name    = reg_flat.name
  reg_offset  =  str(reg_width) + "'h" + "%x" % reg_flat.offset
  reg_msb     = reg_flat.width - 1
  regwen      = reg_flat.regwen
  reg_wr_mask = 0
%>\
  // assertions for register: ${reg_name}
    % if regwen:
<% reg_wen = "`REGWEN_PATH." + regwen + "_qs" %>\
    % else:
<% reg_wen = "1" %>\
    % endif
    % for f in reg_flat.get_fields_flat():
<%
      field_name      = f.name
      assert_path     = reg_name + "." + field_name
      assert_name     = reg_name + "_" + field_name
      field_access    = f.swaccess.name
      field_wr_mask   = ((1 << (f.msb-f.lsb + 1)) -1) << f.lsb
      field_wr_mask_h = format(field_wr_mask, 'x')
      reg_wr_mask    |= field_wr_mask
      reg_wr_mask_h   = format(reg_wr_mask, 'x')
      lsb             = f.lsb
      sw_rdaccess     = f.swrdaccess.name
      had_q           = f.get_n_bits(["q"]) > 0
      has_d           = f.get_n_bits(["d"]) > 0
      has_de          = f.get_n_bits(["de"]) > 0
%>\
      % if not r.ishomog:
        % if r.is_multi_reg():
  // this is a non-homog multi-reg
<%
      mreg_lsb = i * mreg_width_list[loop.index]
      mreg_msb = mreg_lsb + mreg_width_list[loop.index] - 1
%>\
${gen_multi_reg_asserts_by_category(assert_name, mreg_name + "_" + f.get_basename(), mreg_msb, mreg_lsb, reg_flat.hwext, field_wr_mask_h)}\
        % else:
${gen_asserts_by_category(assert_name, assert_path, reg_flat.hwext, field_wr_mask_h)}\
        % endif
      % endif
    % endfor
    % if r.is_multi_reg():
<%
      mreg_lsb = i * (mreg_msb - mreg_lsb + 1)
      mreg_msb = mreg_lsb + reg_msb
      i += 1
%>\
    % endif
    % if r.ishomog:
      % if r.is_multi_reg():
${gen_multi_reg_asserts_by_category(reg_name, mreg_name, mreg_msb, mreg_lsb, reg_flat.hwext, reg_wr_mask_h)}\
      % else:
${gen_asserts_by_category(reg_name, reg_name, reg_flat.hwext, reg_wr_mask_h)}\
      % endif
    % endif
  % endfor
  % endif
% endfor

  `ifdef UVM
    initial forever begin
      bit csr_assert_en;
      uvm_config_db#(bit)::wait_modified(null, "%m", "csr_assert_en");
      if (!uvm_config_db#(bit)::get(null, "%m", "csr_assert_en", csr_assert_en)) begin
        `uvm_fatal("csr_assert", "Can't find csr_assert_en")
      end
      disable_sva = !csr_assert_en;
    end
  `endif

<%def name="gen_asserts_by_category(assert_name, assert_path, is_ext, wr_mask)">\
  % if has_q:
<% reg_w_path = "reg2hw." + assert_path + ".q" %>\
${gen_wr_asserts(assert_name, is_ext, reg_w_path, wr_mask)}\
    % if not has_d:
${gen_rd_asserts(assert_name, is_ext, reg_w_path, wr_mask)}\
    % endif
  % endif
  % if has_d:
    % if has_de and has_q:
<% reg_r_path = "hw2reg." + assert_path + ".de ? hw2reg." + assert_path + ".d :reg2hw." + assert_path + ".q" %>\
${gen_rd_asserts(assert_name, is_ext, reg_r_path, wr_mask)}\
    % elif not has_de:
<% reg_r_path = "hw2reg." + assert_path + ".d" %>\
${gen_rd_asserts(assert_name, is_ext, reg_r_path, wr_mask)}\
    % endif
  % endif
</%def>\
<%def name="gen_multi_reg_asserts_by_category(assert_name, multi_reg_name, mreg_msb, mreg_lsb, is_ext, wr_mask)">\
  % if has_q:
<% reg_w_path = multi_reg_name + "_q_fpv[" + str(mreg_msb) + ":" + str(mreg_lsb) + "]"%>\
${gen_wr_asserts(assert_name, is_ext, reg_w_path, wr_mask)}\
    % if not has_d:
${gen_rd_asserts(assert_name, is_ext, reg_w_path, wr_mask)}\
    % endif
  % endif
  % if has_d:
    % if not has_de:
<% reg_r_path = multi_reg_name + "_d_fpv[" + str(mreg_msb) + ":" + str(mreg_lsb) + "]"%>\
${gen_rd_asserts(assert_name, is_ext, reg_r_path, wr_mask)}\
    % endif
  % endif
</%def>\
<%def name="gen_wr_asserts(name, is_ext, reg_w_path, wr_mask)">\
  % if is_ext:
<% wr_property = "ext_P" %>\
  % else:
<% wr_property = "P" %>\
  % endif
  % if not r.ishomog:
<% shift_index = lsb %>\
  % else:
<% shift_index = 0 %>\
  % endif
  % if field_access == "W1C":
  `ASSERT(${name}_w1c_A, w1c_${wr_property}(${reg_offset}, ${reg_w_path}, ${reg_wen}, 'h${wr_mask}, ${shift_index}), clk_i, !rst_ni || disable_sva)
  % elif field_access in {"RW", "WO", "W0C"}:
  `ASSERT(${name}_wr_A, wr_${wr_property}(${reg_offset}, ${reg_w_path}, ${reg_wen}, 'h${wr_mask}, ${shift_index}), clk_i, !rst_ni || disable_sva)
    % if reg_wen != "1":
  `ASSERT(${name}_wr_regen_A, wr_${wr_property}(${reg_offset}, ${reg_w_path}, ${reg_wen}, 'h${wr_mask}, ${shift_index}), clk_i, !rst_ni || disable_sva)
    % endif
  % endif
</%def>\
<%def name="gen_rd_asserts(name, is_ext, reg_r_path, mask)">\
  % if is_ext:
<% rd_property = "rd_ext_P" %>\
  % else:
<% rd_property = "rd_P" %>\
  % endif
  % if not r.ishomog:
<% shift_index = lsb %>\
  % else:
<% shift_index = 0 %>\
  % endif
  % if sw_rdaccess == "NONE" and field_access == "W1C":
  `ASSERT(${name}_rd_A, ${rd_property}(${reg_offset}, 0, 'h${mask}, ${shift_index}), clk_i, !rst_ni || disable_sva)
  % elif field_access in {"RW", "W0C", "W1C"}:
  `ASSERT(${name}_rd_A, ${rd_property}(${reg_offset}, ${reg_r_path}, 'h${mask}, ${shift_index}), clk_i, !rst_ni || disable_sva)
  % endif
</%def>\
<%def name="declare_fpv_var(name, width, l_index)">\
  % if mreg_has_q_list[l_index]:
  logic [${width}:0] ${name}_q_fpv;
  % endif
  % if mreg_has_d_list[l_index]:
  logic [${width}:0] ${name}_d_fpv;
  % endif
</%def>\
<%def name="assign_fpv_var(fpv_name, dut_path, width, l_index)">\
  % if mreg_has_q_list[l_index]:
    assign ${fpv_name}_q_fpv[((s+1)*${width}-1):s*${width}] = reg2hw.${dut_path}.q;
  % endif
  % if mreg_has_d_list[l_index]:
    assign ${fpv_name}_d_fpv[((s+1)*${width}-1):s*${width}] = hw2reg.${dut_path}.d;
  % endif
</%def>\
</%def>\
${construct_classes(block)}
`undef REGWEN_PATH
`endif
`endif
endmodule