// 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

<% from reggen import (gen_fpv)
%>\
<% from topgen import lib # TODO: Split lib to common lib module
%>\
<%def name="construct_classes(block)">\
% for b in block.blocks:
${construct_classes(b)}
% endfor

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

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

  // mask register to convert byte to bit
  logic [31: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
%>\
  // declare common read and write sequences
  sequence device_wr_S(logic [${addr_msb}:0] addr);
    h2d.a_address == 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);
    h2d.a_address == addr && h2d.a_opcode inside {Get} && h2d.a_valid && h2d.d_ready && !d2h.d_valid;
  endsequence

  // declare common read and write properties
  property wr_P(int width, bit [${addr_msb}:0] addr, bit [31:0] compare_data, bit regen = 1);
    logic [31:0] id;
    logic [width:0] data;
    (device_wr_S(addr),id = h2d.a_source, data = h2d.a_data & a_mask_bit) |->
        strong(##[1:$] (d2h.d_valid && d2h.d_source == id && (d2h.d_error ||
        (!d2h.d_error && compare_data == data) || !regen)));
  endproperty

  property wr_ext_P(int width, bit [${addr_msb}:0] addr, bit [31:0] compare_data, bit regen = 1);
    logic [31:0] id;
    logic [width:0] data;
    logic [width:0] compare_value;
    (device_wr_S(addr),id = h2d.a_source, data = h2d.a_data & a_mask_bit,
        compare_value = compare_data) |->
        strong(##[1:$] (d2h.d_valid && d2h.d_source == id && (d2h.d_error ||
        (!d2h.d_error && compare_value == data) || !regen)));
  endproperty

  property rd_P(int width, bit [${addr_msb}:0] addr, bit [31:0] compare_data);
    logic [31:0] id;
    logic [width:0] data;
    (device_rd_S(addr), id = h2d.a_source, data = $past(compare_data)) |->
        strong(##[1:$] (d2h.d_valid && d2h.d_source == id && (d2h.d_error ||
        (!d2h.d_error && d2h.d_data == data))));
  endproperty

  property rd_ext_P(int width, bit [${addr_msb}:0] addr, bit [31:0] compare_data);
    logic [31:0] id;
    logic [width:0] data;
    (device_rd_S(addr), id = h2d.a_source, data = compare_data) |->
        strong(##[1:$] (d2h.d_valid && d2h.d_source == id && (d2h.d_error ||
        (!d2h.d_error && d2h.d_data == data))));
  endproperty

  property wr_regen_stable_P(regen, compare_data);
    (!regen && $stable(regen)) |-> $stable(compare_data);
  endproperty

// for all the regsters, declare assertion
% for r in block.regs:
<%
  i = -1
  msb = -1
  lsb = 0
%>\
  % for reg_flat in r.get_regs_flat():
<%
  reg_name = reg_flat.name
  reg_right = reg_flat.dvrights
  reg_width = block.addr_width
  reg_offset =  str(reg_width) + "'h" + "%x" % reg_flat.offset
  reg_msb = reg_flat.width - 1
  hwaccess = reg_flat.fields[0].hwaccess
  regwen = reg_flat.regwen
%>\
    % if regwen:
<%
    reg_wen = "i_"+ block.name + ".i_reg_top."+ regwen + "_qs"
%>\
    % else:
<%
    reg_wen = "0"
%>\
    % endif
    % if r.is_multi_reg():
<%
      r_multi_name = r.name
      f = reg_flat.fields[0]
      r_multi_width = f.msb - f.lsb + 1
      r_multi_depth = r.get_n_fields_flat()
      r_multi_msb = r_multi_width * r_multi_depth -1
      i += 1
      lsb = i * (msb - lsb + 1)
      msb = lsb + reg_msb
      reg_d_path = r_multi_name + "_d_fpv[" + str(msb) + ":" + str(lsb) + "]"
      reg_q_path = r_multi_name + "_q_fpv[" + str(msb) + ":" + str(lsb) + "]"
%>\
      % if (i == 0):

  // define local fpv variable for the multi_reg
        % if reg_flat.get_n_bits(["q"]):
  logic [${r_multi_msb}:0] ${r_multi_name}_q_fpv;
          % if r_multi_width == 1:
  for (genvar s = 0; s <= ${r_multi_msb}; s++) begin : gen_${r_multi_name}_rd
    assign ${r_multi_name}_q_fpv[s] = i_${block.name}.reg2hw.${r_multi_name}[s].q;
          % else:
  for (genvar s = 0; s <= ${r_multi_depth}-1; s++) begin : gen_${r_multi_name}_rd
    assign ${r_multi_name}_q_fpv[((s+1)*${r_multi_width}-1):s*${r_multi_width}] = i_${block.name}.reg2hw.${r_multi_name}[s].q;
          % endif
  end
        % endif
        % if reg_flat.get_n_bits(["d"]):
  logic [${r_multi_msb}:0] ${r_multi_name}_d_fpv;
          % if r_multi_width == 1:
  for (genvar s = 0; s <= ${r_multi_msb}; s++) begin : gen_${r_multi_name}_wr
    assign ${r_multi_name}_d_fpv[s] = i_${block.name}.hw2reg.${r_multi_name}[s].d;
          % else:
  for (genvar s = 0; s <= ${r_multi_depth}-1; s++) begin : gen_${r_multi_name}_wr
    assign ${r_multi_name}_d_fpv[(s*${r_multi_width}-1):s] = i_${block.name}.hw2reg.${r_multi_name}[s].d;
          % endif
  end
        % endif
      % endif
    % else :
<%
      reg_d_path = "i_" + block.name + ".hw2reg." + reg_name + ".d"
      reg_q_path = "i_" + block.name + ".reg2hw." + reg_name + ".q"
%>\
    % endif
    % if reg_flat.hwext:
<%
      wr_prperty = "wr_ext_P"
      rd_prperty = "rd_ext_P"
%>\
    % else:
<%
      wr_prperty = "wr_P"
      rd_prperty = "rd_P"
%>\
    % endif

    % if reg_flat.get_n_bits(["q", "d"]) == 0:
<%
      reg_we_path = "i_" + block.name + ".i_reg_top." + reg_name + "_we"
      reg_qs_path = "i_" + block.name + ".i_reg_top." + reg_name + "_qs"
%>\
    % endif
  // read/write assertions for register: ${reg_name}
    % if reg_flat.dvrights in {"RW", "WO"}:
      % if reg_flat.get_n_bits(["q", "d"]) == 0:
  `ASSERT(${reg_name}_wr_A, ${wr_prperty}(${reg_msb}, ${reg_offset}, ${reg_we_path}, ${reg_wen}), clk_i, !rst_ni)
      % else:
  `ASSERT(${reg_name}_wr_A, ${wr_prperty}(${reg_msb}, ${reg_offset}, ${reg_q_path}, ${reg_wen}), clk_i, !rst_ni)
      % endif
      % if regwen:
  `ASSERT(${reg_name}_stable_A, wr_regen_stable_P(${reg_wen}, ${reg_q_path}), clk_i, !rst_ni)
      % endif
    % endif
    % if reg_flat.dvrights in {"RW", "RO"}:
      % if reg_flat.get_n_bits(["q", "d"]) == 0:
  `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_qs_path}), clk_i, !rst_ni)
      % elif reg_flat.get_n_bits(["d"]):
  `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_d_path}), clk_i, !rst_ni)
      % elif reg_flat.get_n_bits(["q"]) and (r.ishomog or ((not r.ishomog) and r.get_fields_flat()[0].get_n_bits(["q"]))):
  `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_msb}, ${reg_offset}, ${reg_q_path}), clk_i, !rst_ni)
      % endif
    % endif
  % endfor
% endfor
</%def>\
${construct_classes(block)}
endmodule