// 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
%>\
<%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::*; (
  input clk_i,
  input rst_ni,

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

  parameter int DWidth = 32;
  // mask register to convert byte to bit
  logic [DWidth-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
  mask = block.addr_width
%>\
  // 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

  // this sequence is used for reg_field which has access w1c or w0c
  // it returns true if the `index` bit of a_data matches `exp_bit`
  // this sequence is under assumption - w1c/w0c will only use one bit per field
  sequence device_wc_S(logic [${addr_msb}:0] addr, bit exp_bit, int index);
    h2d.a_address == addr && h2d.a_opcode inside {PutFullData, PutPartialData} && h2d.a_valid &&
        h2d.d_ready && !d2h.d_valid && ((h2d.a_data[index] & a_mask_bit[index]) == exp_bit);
  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(bit [${addr_msb}:0] addr, bit [DWidth-1:0] act_data, bit regen,
                bit [DWidth-1:0] mask);
    logic [DWidth-1:0] id, exp_data;
    (device_wr_S(addr), 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 == exp_data || !regen);
  endproperty

  // external reg will use one clk cycle to update act_data from external
  property wr_ext_P(bit [${addr_msb}:0] addr, bit [DWidth-1:0] act_data, bit regen,
                    bit [DWidth-1:0] mask);
    logic [DWidth-1:0] id, exp_data;
    (device_wr_S(addr), 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) == exp_data || !regen);
  endproperty

  // For W1C or W0C, first scenario: write 1(W1C) or 0(W0C) that clears the value
  property wc0_P(bit [${addr_msb}:0] addr, bit act_data, bit regen, int index, bit clear_bit);
    logic [DWidth-1:0] id;
    (device_wc_S(addr, clear_bit, index), id = h2d.a_source) ##1
        first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
        (d2h.d_error || act_data == 1'b0 || !regen);
  endproperty

  // For W1C or W0C, second scenario: write 0(W1C) or 1(W0C) that won't clear the value
  property wc1_P(bit [${addr_msb}:0] addr, bit act_data, bit regen, int index, bit clear_bit);
    logic [DWidth-1:0] id;
    (device_wc_S(addr, !clear_bit, index), id = h2d.a_source) ##1
        first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
        (d2h.d_error || $stable(act_data) || !regen);
  endproperty

  property rd_P(bit [${addr_msb}:0] addr, bit [DWidth-1:0] act_data);
    logic [DWidth-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 == exp_data);
  endproperty

  property rd_ext_P(bit [${addr_msb}:0] addr, bit [DWidth-1:0] act_data);
    logic [DWidth-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 == exp_data);
  endproperty

  // read a WO register, always return 0
  property r_wo_P(bit [${addr_msb}:0] addr);
    logic [DWidth-1:0] id;
    (device_rd_S(addr), id = h2d.a_source) ##1
        first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
        (d2h.d_error || d2h.d_data == 0);
  endproperty

  property wr_regen_stable_P(bit regen, bit [DWidth-1:0] exp_data);
    (!regen && $stable(regen)) |-> $stable(exp_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_width = block.addr_width
  reg_offset =  str(reg_width) + "'h" + "%x" % reg_flat.offset
  reg_msb = reg_flat.width - 1
  regwen = reg_flat.regwen
  reg_access = set()
  reg_wr_mask = 0
  hw_access = reg_flat.fields[0].hwaccess
%>\
    % if regwen:
<%
    reg_wen = "i_"+ block.name + ".i_reg_top."+ regwen + "_qs"
%>\
    % else:
<%
    reg_wen = "1"
%>\
    % 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
%>\
      % if reg_flat.get_n_bits(["q"]):
<%
      reg_r_path = r_multi_name + "_q_fpv[" + str(msb) + ":" + str(lsb) + "]"
      reg_w_path = r_multi_name + "_q_fpv[" + str(msb) + ":" + str(lsb) + "]"
%>\
      % endif
      % if reg_flat.get_n_bits(["d"]):
<%
      reg_r_path = r_multi_name + "_d_fpv[" + str(msb) + ":" + str(lsb) + "]"
%>\
      % endif
      % 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 reg_flat.get_n_bits(["qe"]):
<%
      qe = "i_" + block.name + ".reg2hw." + r_multi_name + "[s].qe"
%>\
          % else:
<%
      qe = 1
%>\
          % endif
          % if r_multi_width == 1:
  for (genvar s = 0; s <= ${r_multi_msb}; s++) begin : gen_${r_multi_name}_q
    assign ${r_multi_name}_q_fpv[s] = ${qe} ?
        i_${block.name}.reg2hw.${r_multi_name}[s].q : ${r_multi_name}_q_fpv[s];
          % else:
  for (genvar s = 0; s < ${r_multi_depth}; s++) begin : gen_${r_multi_name}_q
    assign ${r_multi_name}_q_fpv[((s+1)*${r_multi_width}-1):s*${r_multi_width}] = ${qe} ?
        i_${block.name}.reg2hw.${r_multi_name}[s].q : ${r_multi_name}_q_fpv[((s+1)*${r_multi_width}-1):s*${r_multi_width}];
          % 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}_d
    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}_d
    assign ${r_multi_name}_d_fpv[((s+1)*${r_multi_width}-1):s*${r_multi_width}] = i_${block.name}.hw2reg.${r_multi_name}[s].d;
          % endif
  end
        % endif
      % endif
    % else :
<%
      reg_r_path = "i_" + block.name + ".hw2reg." + reg_name + ".d"
      reg_w_path = "i_" + block.name + ".reg2hw." + reg_name + ".q"
%>\
      % if hw_access == HwAccess.HRO or hw_access == HwAccess.NONE:
<%
      reg_r_path = "i_" + block.name + ".reg2hw." + reg_name + ".q"
%>\
      % endif
      % if reg_flat.get_n_bits(["q", "d"]) == 0:
<%
      reg_r_path = "i_" + block.name + ".i_reg_top." + reg_name + "_qs"
      reg_w_path = "i_" + block.name + ".i_reg_top." + reg_name + "_qs"
%>\
      % endif
    % 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
    % for f in reg_flat.get_fields_flat():
<%
        field_access = f.swaccess.name
        reg_access.add(field_access)
        reg_wr_mask |= ((1 << (f.msb-f.lsb + 1)) -1) << f.lsb
%>\
      % if field_access == "W0C":
  // assertions for W0C reg fields:
  `ASSERT(${f.name}_wc0_A, wc0_P(${reg_offset}, ${reg_w_path}, ${reg_wen}, ${f.lsb}, 0))
  `ASSERT(${f.name}_wc1_A, wc1_P(${reg_offset}, ${reg_w_path}, ${reg_wen}, ${f.lsb}, 0))
  `ASSERT(${f.name}_rd_A, ${rd_prperty}(${reg_offset}, ${reg_r_path}))
      % elif field_access == "W1C":
  // assertions for W1C reg fields:
  `ASSERT(${f.name}_wc0_A, wc0_P(${reg_offset}, ${reg_w_path}, ${reg_wen}, ${f.lsb}, 1))
  `ASSERT(${f.name}_wc1_A, wc1_P(${reg_offset}, ${reg_w_path}, ${reg_wen}, ${f.lsb}, 1))
  `ASSERT(${f.name}_rd_A, ${rd_prperty}(${reg_offset}, ${reg_r_path}))
      % endif
    % endfor
<%
      reg_wr_mask_h = format(reg_wr_mask, 'x')
%>\

    % if "RW" in reg_access:
  `ASSERT(${reg_name}_wr_A, ${wr_prperty}(${reg_offset}, ${reg_w_path}, ${reg_wen}, 'h${reg_wr_mask_h}))
  `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_offset}, ${reg_r_path}))
    % elif "WO" in reg_access:
  `ASSERT(${reg_name}_wr_A, ${wr_prperty}(${reg_offset}, ${reg_w_path}, ${reg_wen}, 'h${reg_wr_mask_h}))
  `ASSERT(${reg_name}_rd_A, r_wo_P(${reg_offset}))
    % elif "RO" in reg_access:
  `ASSERT(${reg_name}_rd_A, ${rd_prperty}(${reg_offset}, ${reg_r_path}))
    % endif
    % if regwen:
  `ASSERT(${reg_name}_stable_A, wr_regen_stable_P(${reg_wen}, ${reg_w_path}))
    % endif
  % endfor
% endfor
</%def>\
${construct_classes(block)}
endmodule