[fpv] generate csr_assert on the fly
This PR uses PR #2941 method to generate csr assertions on the fly for
FPV testbenches.
This change includes: rv_plic, pinmux, padctrl, rv_plic top_level
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/ip/padctrl/fpv/padctrl_fpv.core b/hw/ip/padctrl/fpv/padctrl_fpv.core
index f3c9889..07e33dd 100644
--- a/hw/ip/padctrl/fpv/padctrl_fpv.core
+++ b/hw/ip/padctrl/fpv/padctrl_fpv.core
@@ -12,14 +12,21 @@
# from a particular top-level config
- lowrisc:ip:padctrl
- lowrisc:prim:prim_pkg
+ - lowrisc:fpv:csr_assert_gen
files:
- tb/padctrl_fpv.sv
- tb/padctrl_bind_fpv.sv
- vip/padctrl_assert_fpv.sv
- vip/padring_assert_fpv.sv
- - vip/padctrl_csr_assert_fpv.sv
file_type: systemVerilogSource
+generate:
+ csr_assert_gen:
+ generator: csr_assert_gen
+ parameters:
+ spec: ../data/padctrl.hjson
+ depend: lowrisc:ip:padctrl_reg
+
targets:
default: &default_target
# note, this setting is just used
@@ -27,7 +34,9 @@
default_tool: icarus
filesets:
- files_formal
- toplevel: padctrl_formal
+ generate:
+ - csr_assert_gen
+ toplevel: padctrl_fpv
formal:
<<: *default_target
diff --git a/hw/ip/padctrl/fpv/vip/padctrl_csr_assert_fpv.sv b/hw/ip/padctrl/fpv/vip/padctrl_csr_assert_fpv.sv
deleted file mode 100644
index cdf1901..0000000
--- a/hw/ip/padctrl/fpv/vip/padctrl_csr_assert_fpv.sv
+++ /dev/null
@@ -1,160 +0,0 @@
-// 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 and regwen reg
-// This automation assumes that W1C and W0C are registers with 1 bit per field
-
-`include "prim_assert.sv"
-
-// Block: padctrl
-module padctrl_csr_assert_fpv import tlul_pkg::*; import padctrl_reg_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 padctrl_reg2hw_t reg2hw,
- input padctrl_hw2reg_t hw2reg
-);
-
- 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;
-
- // declare common read and write sequences
- sequence device_wr_S(logic [5: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 [5: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
- // 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 [5:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- 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 << lsb) == exp_data || !regen);
- endproperty
-
- // external reg will use one clk cycle to update act_data from external
- property wr_ext_P(bit [5:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- 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) << lsb) == exp_data || !regen);
- endproperty
-
- property w1c_P(bit [5:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- logic [DWidth-1:0] id, exp_data;
- (device_wr_S(addr), id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask & '0) ##1
- first_match(##[0:$] d2h.d_valid && d2h.d_source == id) |->
- (d2h.d_error || (act_data << lsb) == exp_data || !regen);
- endproperty
-
- property w1c_ext_P(bit [5:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- logic [DWidth-1:0] id, exp_data;
- (device_wr_S(addr), id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask & '0) ##1
- first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
- (d2h.d_error || ($past(act_data) << lsb) == exp_data || !regen);
- endproperty
-
- property rd_P(bit [5:0] addr, bit [DWidth-1:0] act_data, bit [DWidth-1:0] mask, int lsb);
- 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 & mask) >> lsb == exp_data);
- endproperty
-
- property rd_ext_P(bit [5:0] addr, bit [DWidth-1:0] act_data, bit [DWidth-1:0] mask,
- int lsb);
- 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 & mask) >> lsb == exp_data);
- endproperty
-
- // read a WO register, always return 0
- property r_wo_P(bit [5: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
-
- // TODO: currently not used, will use once support regwen reg
- property wr_regen_stable_P(bit regen, bit [DWidth-1:0] exp_data);
- (!regen && $stable(regen)) |-> $stable(exp_data);
- endproperty
-
-
- // assertions for register: regen
-
- // define local fpv variable for multi-reg
- logic [39:0] dio_pads_q_fpv;
- logic [39:0] dio_pads_d_fpv;
- for (genvar s = 0; s < 4; s++) begin : gen_dio_pads_q
- assign dio_pads_q_fpv[((s+1)*10-1):s*10] = reg2hw.dio_pads[s].q;
- assign dio_pads_d_fpv[((s+1)*10-1):s*10] = hw2reg.dio_pads[s].d;
- end
-
- // assertions for register: dio_pads0
- `ASSERT(dio_pads0_wr_A, wr_ext_P(6'h4, dio_pads_q_fpv[29:0], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(dio_pads0_rd_A, rd_ext_P(6'h4, dio_pads_d_fpv[29:0], 'h3fffffff, 0))
- // assertions for register: dio_pads1
- `ASSERT(dio_pads1_wr_A, wr_ext_P(6'h8, dio_pads_q_fpv[39:30], dut.u_reg.regen_qs, 'h3ff, 0))
- `ASSERT(dio_pads1_rd_A, rd_ext_P(6'h8, dio_pads_d_fpv[39:30], 'h3ff, 0))
-
- // define local fpv variable for multi-reg
- logic [159:0] mio_pads_q_fpv;
- logic [159:0] mio_pads_d_fpv;
- for (genvar s = 0; s < 16; s++) begin : gen_mio_pads_q
- assign mio_pads_q_fpv[((s+1)*10-1):s*10] = reg2hw.mio_pads[s].q;
- assign mio_pads_d_fpv[((s+1)*10-1):s*10] = hw2reg.mio_pads[s].d;
- end
-
- // assertions for register: mio_pads0
- `ASSERT(mio_pads0_wr_A, wr_ext_P(6'hc, mio_pads_q_fpv[29:0], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_pads0_rd_A, rd_ext_P(6'hc, mio_pads_d_fpv[29:0], 'h3fffffff, 0))
- // assertions for register: mio_pads1
- `ASSERT(mio_pads1_wr_A, wr_ext_P(6'h10, mio_pads_q_fpv[59:30], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_pads1_rd_A, rd_ext_P(6'h10, mio_pads_d_fpv[59:30], 'h3fffffff, 0))
- // assertions for register: mio_pads2
- `ASSERT(mio_pads2_wr_A, wr_ext_P(6'h14, mio_pads_q_fpv[89:60], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_pads2_rd_A, rd_ext_P(6'h14, mio_pads_d_fpv[89:60], 'h3fffffff, 0))
- // assertions for register: mio_pads3
- `ASSERT(mio_pads3_wr_A, wr_ext_P(6'h18, mio_pads_q_fpv[119:90], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_pads3_rd_A, rd_ext_P(6'h18, mio_pads_d_fpv[119:90], 'h3fffffff, 0))
- // assertions for register: mio_pads4
- `ASSERT(mio_pads4_wr_A, wr_ext_P(6'h1c, mio_pads_q_fpv[149:120], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_pads4_rd_A, rd_ext_P(6'h1c, mio_pads_d_fpv[149:120], 'h3fffffff, 0))
- // assertions for register: mio_pads5
- `ASSERT(mio_pads5_wr_A, wr_ext_P(6'h20, mio_pads_q_fpv[159:150], dut.u_reg.regen_qs, 'h3ff, 0))
- `ASSERT(mio_pads5_rd_A, rd_ext_P(6'h20, mio_pads_d_fpv[159:150], 'h3ff, 0))
-
-
-endmodule
diff --git a/hw/ip/pinmux/fpv/pinmux_fpv.core b/hw/ip/pinmux/fpv/pinmux_fpv.core
index e31ecd9..dc7f03c 100644
--- a/hw/ip/pinmux/fpv/pinmux_fpv.core
+++ b/hw/ip/pinmux/fpv/pinmux_fpv.core
@@ -5,23 +5,32 @@
name: "lowrisc:fpv:pinmux_fpv:0.1"
description: "pinmux FPV target"
filesets:
- files_fpv:
+ files_formal:
depend:
- lowrisc:prim:all
- lowrisc:ip:tlul
- lowrisc:ip:pinmux
+ - lowrisc:fpv:csr_assert_gen
files:
- vip/pinmux_assert_fpv.sv
- tb/pinmux_bind_fpv.sv
- tb/pinmux_fpv.sv
- - vip/pinmux_csr_assert_fpv.sv
file_type: systemVerilogSource
+generate:
+ csr_assert_gen:
+ generator: csr_assert_gen
+ parameters:
+ spec: ../data/pinmux.hjson
+ depend: lowrisc:ip:pinmux_reg
+
targets:
default: &default_target
default_tool: icarus
filesets:
- - files_fpv
+ - files_formal
+ generate:
+ - csr_assert_gen
toplevel: pinmux_fpv
formal:
diff --git a/hw/ip/pinmux/fpv/vip/pinmux_csr_assert_fpv.sv b/hw/ip/pinmux/fpv/vip/pinmux_csr_assert_fpv.sv
deleted file mode 100644
index 0130006..0000000
--- a/hw/ip/pinmux/fpv/vip/pinmux_csr_assert_fpv.sv
+++ /dev/null
@@ -1,338 +0,0 @@
-// 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 and regwen reg
-// This automation assumes that W1C and W0C are registers with 1 bit per field
-
-`include "prim_assert.sv"
-
-// Block: pinmux
-module pinmux_csr_assert_fpv import tlul_pkg::*; import pinmux_reg_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 pinmux_reg2hw_t reg2hw,
- input pinmux_hw2reg_t hw2reg
-);
-
- 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;
-
- // declare common read and write sequences
- sequence device_wr_S(logic [6: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 [6: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
- // 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 [6:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- 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 << lsb) == exp_data || !regen);
- endproperty
-
- // external reg will use one clk cycle to update act_data from external
- property wr_ext_P(bit [6:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- 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) << lsb) == exp_data || !regen);
- endproperty
-
- property w1c_P(bit [6:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- logic [DWidth-1:0] id, exp_data;
- (device_wr_S(addr), id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask & '0) ##1
- first_match(##[0:$] d2h.d_valid && d2h.d_source == id) |->
- (d2h.d_error || (act_data << lsb) == exp_data || !regen);
- endproperty
-
- property w1c_ext_P(bit [6:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- logic [DWidth-1:0] id, exp_data;
- (device_wr_S(addr), id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask & '0) ##1
- first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
- (d2h.d_error || ($past(act_data) << lsb) == exp_data || !regen);
- endproperty
-
- property rd_P(bit [6:0] addr, bit [DWidth-1:0] act_data, bit [DWidth-1:0] mask, int lsb);
- 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 & mask) >> lsb == exp_data);
- endproperty
-
- property rd_ext_P(bit [6:0] addr, bit [DWidth-1:0] act_data, bit [DWidth-1:0] mask,
- int lsb);
- 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 & mask) >> lsb == exp_data);
- endproperty
-
- // read a WO register, always return 0
- property r_wo_P(bit [6: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
-
- // TODO: currently not used, will use once support regwen reg
- property wr_regen_stable_P(bit regen, bit [DWidth-1:0] exp_data);
- (!regen && $stable(regen)) |-> $stable(exp_data);
- endproperty
-
-
- // assertions for register: regen
-
- // define local fpv variable for multi-reg
- logic [191:0] periph_insel_q_fpv;
- for (genvar s = 0; s < 32; s++) begin : gen_periph_insel_q
- assign periph_insel_q_fpv[((s+1)*6-1):s*6] = reg2hw.periph_insel[s].q;
- end
-
- // assertions for register: periph_insel0
- `ASSERT(periph_insel0_wr_A, wr_P(7'h4, periph_insel_q_fpv[29:0], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(periph_insel0_rd_A, rd_P(7'h4, periph_insel_q_fpv[29:0], 'h3fffffff, 0))
- // assertions for register: periph_insel1
- `ASSERT(periph_insel1_wr_A, wr_P(7'h8, periph_insel_q_fpv[59:30], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(periph_insel1_rd_A, rd_P(7'h8, periph_insel_q_fpv[59:30], 'h3fffffff, 0))
- // assertions for register: periph_insel2
- `ASSERT(periph_insel2_wr_A, wr_P(7'hc, periph_insel_q_fpv[89:60], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(periph_insel2_rd_A, rd_P(7'hc, periph_insel_q_fpv[89:60], 'h3fffffff, 0))
- // assertions for register: periph_insel3
- `ASSERT(periph_insel3_wr_A, wr_P(7'h10, periph_insel_q_fpv[119:90], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(periph_insel3_rd_A, rd_P(7'h10, periph_insel_q_fpv[119:90], 'h3fffffff, 0))
- // assertions for register: periph_insel4
- `ASSERT(periph_insel4_wr_A, wr_P(7'h14, periph_insel_q_fpv[149:120], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(periph_insel4_rd_A, rd_P(7'h14, periph_insel_q_fpv[149:120], 'h3fffffff, 0))
- // assertions for register: periph_insel5
- `ASSERT(periph_insel5_wr_A, wr_P(7'h18, periph_insel_q_fpv[179:150], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(periph_insel5_rd_A, rd_P(7'h18, periph_insel_q_fpv[179:150], 'h3fffffff, 0))
- // assertions for register: periph_insel6
- `ASSERT(periph_insel6_wr_A, wr_P(7'h1c, periph_insel_q_fpv[191:180], dut.u_reg.regen_qs, 'hfff, 0))
- `ASSERT(periph_insel6_rd_A, rd_P(7'h1c, periph_insel_q_fpv[191:180], 'hfff, 0))
-
- // define local fpv variable for multi-reg
- logic [191:0] mio_outsel_q_fpv;
- for (genvar s = 0; s < 32; s++) begin : gen_mio_outsel_q
- assign mio_outsel_q_fpv[((s+1)*6-1):s*6] = reg2hw.mio_outsel[s].q;
- end
-
- // assertions for register: mio_outsel0
- `ASSERT(mio_outsel0_wr_A, wr_P(7'h20, mio_outsel_q_fpv[29:0], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_outsel0_rd_A, rd_P(7'h20, mio_outsel_q_fpv[29:0], 'h3fffffff, 0))
- // assertions for register: mio_outsel1
- `ASSERT(mio_outsel1_wr_A, wr_P(7'h24, mio_outsel_q_fpv[59:30], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_outsel1_rd_A, rd_P(7'h24, mio_outsel_q_fpv[59:30], 'h3fffffff, 0))
- // assertions for register: mio_outsel2
- `ASSERT(mio_outsel2_wr_A, wr_P(7'h28, mio_outsel_q_fpv[89:60], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_outsel2_rd_A, rd_P(7'h28, mio_outsel_q_fpv[89:60], 'h3fffffff, 0))
- // assertions for register: mio_outsel3
- `ASSERT(mio_outsel3_wr_A, wr_P(7'h2c, mio_outsel_q_fpv[119:90], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_outsel3_rd_A, rd_P(7'h2c, mio_outsel_q_fpv[119:90], 'h3fffffff, 0))
- // assertions for register: mio_outsel4
- `ASSERT(mio_outsel4_wr_A, wr_P(7'h30, mio_outsel_q_fpv[149:120], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_outsel4_rd_A, rd_P(7'h30, mio_outsel_q_fpv[149:120], 'h3fffffff, 0))
- // assertions for register: mio_outsel5
- `ASSERT(mio_outsel5_wr_A, wr_P(7'h34, mio_outsel_q_fpv[179:150], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(mio_outsel5_rd_A, rd_P(7'h34, mio_outsel_q_fpv[179:150], 'h3fffffff, 0))
- // assertions for register: mio_outsel6
- `ASSERT(mio_outsel6_wr_A, wr_P(7'h38, mio_outsel_q_fpv[191:180], dut.u_reg.regen_qs, 'hfff, 0))
- `ASSERT(mio_outsel6_rd_A, rd_P(7'h38, mio_outsel_q_fpv[191:180], 'hfff, 0))
-
- // define local fpv variable for multi-reg
- logic [63:0] mio_out_sleep_val_q_fpv;
- for (genvar s = 0; s < 32; s++) begin : gen_mio_out_sleep_val_q
- assign mio_out_sleep_val_q_fpv[((s+1)*2-1):s*2] = reg2hw.mio_out_sleep_val[s].q;
- end
-
- // assertions for register: mio_out_sleep_val0
- `ASSERT(mio_out_sleep_val0_wr_A, wr_P(7'h3c, mio_out_sleep_val_q_fpv[31:0], dut.u_reg.regen_qs, 'hffffffff, 0))
- `ASSERT(mio_out_sleep_val0_rd_A, rd_P(7'h3c, mio_out_sleep_val_q_fpv[31:0], 'hffffffff, 0))
- // assertions for register: mio_out_sleep_val1
- `ASSERT(mio_out_sleep_val1_wr_A, wr_P(7'h40, mio_out_sleep_val_q_fpv[63:32], dut.u_reg.regen_qs, 'hffffffff, 0))
- `ASSERT(mio_out_sleep_val1_rd_A, rd_P(7'h40, mio_out_sleep_val_q_fpv[63:32], 'hffffffff, 0))
-
- // define local fpv variable for multi-reg
- logic [31:0] dio_out_sleep_val_q_fpv;
- logic [31:0] dio_out_sleep_val_d_fpv;
- for (genvar s = 0; s < 16; s++) begin : gen_dio_out_sleep_val_q
- assign dio_out_sleep_val_q_fpv[((s+1)*2-1):s*2] = reg2hw.dio_out_sleep_val[s].q;
- assign dio_out_sleep_val_d_fpv[((s+1)*2-1):s*2] = hw2reg.dio_out_sleep_val[s].d;
- end
-
- // assertions for register: dio_out_sleep_val
- `ASSERT(dio_out_sleep_val_wr_A, wr_ext_P(7'h44, dio_out_sleep_val_q_fpv[31:0], dut.u_reg.regen_qs, 'hffffffff, 0))
- `ASSERT(dio_out_sleep_val_rd_A, rd_ext_P(7'h44, dio_out_sleep_val_d_fpv[31:0], 'hffffffff, 0))
-
- // define local fpv variable for multi-reg
- logic [7:0] wkup_detector_en_q_fpv;
- for (genvar s = 0; s < 8; s++) begin : gen_wkup_detector_en_q
- assign wkup_detector_en_q_fpv[((s+1)*1-1):s*1] = reg2hw.wkup_detector_en[s].q;
- end
-
- // assertions for register: wkup_detector_en
- `ASSERT(wkup_detector_en_wr_A, wr_P(7'h48, wkup_detector_en_q_fpv[7:0], dut.u_reg.regen_qs, 'hff, 0))
- `ASSERT(wkup_detector_en_rd_A, rd_P(7'h48, wkup_detector_en_q_fpv[7:0], 'hff, 0))
-
- // define local fpv variable for multi-reg
- logic [23:0] wkup_detector_mode_q_fpv;
- logic [7:0] wkup_detector_filter_q_fpv;
- logic [7:0] wkup_detector_miodio_q_fpv;
- for (genvar s = 0; s < 8; s++) begin : gen_wkup_detector_q
- assign wkup_detector_mode_q_fpv[((s+1)*3-1):s*3] = reg2hw.wkup_detector[s].mode.q;
- assign wkup_detector_filter_q_fpv[((s+1)*1-1):s*1] = reg2hw.wkup_detector[s].filter.q;
- assign wkup_detector_miodio_q_fpv[((s+1)*1-1):s*1] = reg2hw.wkup_detector[s].miodio.q;
- end
-
- // assertions for register: wkup_detector0
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector0_mode0_wr_A, wr_P(7'h4c, wkup_detector_mode_q_fpv[2:0], dut.u_reg.regen_qs, 'h7, 0))
- `ASSERT(wkup_detector0_mode0_rd_A, rd_P(7'h4c, wkup_detector_mode_q_fpv[2:0], 'h7, 0))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector0_filter0_wr_A, wr_P(7'h4c, wkup_detector_filter_q_fpv[0:0], dut.u_reg.regen_qs, 'h8, 3))
- `ASSERT(wkup_detector0_filter0_rd_A, rd_P(7'h4c, wkup_detector_filter_q_fpv[0:0], 'h8, 3))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector0_miodio0_wr_A, wr_P(7'h4c, wkup_detector_miodio_q_fpv[0:0], dut.u_reg.regen_qs, 'h10, 4))
- `ASSERT(wkup_detector0_miodio0_rd_A, rd_P(7'h4c, wkup_detector_miodio_q_fpv[0:0], 'h10, 4))
- // assertions for register: wkup_detector1
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector1_mode1_wr_A, wr_P(7'h50, wkup_detector_mode_q_fpv[5:3], dut.u_reg.regen_qs, 'h7, 0))
- `ASSERT(wkup_detector1_mode1_rd_A, rd_P(7'h50, wkup_detector_mode_q_fpv[5:3], 'h7, 0))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector1_filter1_wr_A, wr_P(7'h50, wkup_detector_filter_q_fpv[1:1], dut.u_reg.regen_qs, 'h8, 3))
- `ASSERT(wkup_detector1_filter1_rd_A, rd_P(7'h50, wkup_detector_filter_q_fpv[1:1], 'h8, 3))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector1_miodio1_wr_A, wr_P(7'h50, wkup_detector_miodio_q_fpv[1:1], dut.u_reg.regen_qs, 'h10, 4))
- `ASSERT(wkup_detector1_miodio1_rd_A, rd_P(7'h50, wkup_detector_miodio_q_fpv[1:1], 'h10, 4))
- // assertions for register: wkup_detector2
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector2_mode2_wr_A, wr_P(7'h54, wkup_detector_mode_q_fpv[8:6], dut.u_reg.regen_qs, 'h7, 0))
- `ASSERT(wkup_detector2_mode2_rd_A, rd_P(7'h54, wkup_detector_mode_q_fpv[8:6], 'h7, 0))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector2_filter2_wr_A, wr_P(7'h54, wkup_detector_filter_q_fpv[2:2], dut.u_reg.regen_qs, 'h8, 3))
- `ASSERT(wkup_detector2_filter2_rd_A, rd_P(7'h54, wkup_detector_filter_q_fpv[2:2], 'h8, 3))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector2_miodio2_wr_A, wr_P(7'h54, wkup_detector_miodio_q_fpv[2:2], dut.u_reg.regen_qs, 'h10, 4))
- `ASSERT(wkup_detector2_miodio2_rd_A, rd_P(7'h54, wkup_detector_miodio_q_fpv[2:2], 'h10, 4))
- // assertions for register: wkup_detector3
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector3_mode3_wr_A, wr_P(7'h58, wkup_detector_mode_q_fpv[11:9], dut.u_reg.regen_qs, 'h7, 0))
- `ASSERT(wkup_detector3_mode3_rd_A, rd_P(7'h58, wkup_detector_mode_q_fpv[11:9], 'h7, 0))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector3_filter3_wr_A, wr_P(7'h58, wkup_detector_filter_q_fpv[3:3], dut.u_reg.regen_qs, 'h8, 3))
- `ASSERT(wkup_detector3_filter3_rd_A, rd_P(7'h58, wkup_detector_filter_q_fpv[3:3], 'h8, 3))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector3_miodio3_wr_A, wr_P(7'h58, wkup_detector_miodio_q_fpv[3:3], dut.u_reg.regen_qs, 'h10, 4))
- `ASSERT(wkup_detector3_miodio3_rd_A, rd_P(7'h58, wkup_detector_miodio_q_fpv[3:3], 'h10, 4))
- // assertions for register: wkup_detector4
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector4_mode4_wr_A, wr_P(7'h5c, wkup_detector_mode_q_fpv[14:12], dut.u_reg.regen_qs, 'h7, 0))
- `ASSERT(wkup_detector4_mode4_rd_A, rd_P(7'h5c, wkup_detector_mode_q_fpv[14:12], 'h7, 0))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector4_filter4_wr_A, wr_P(7'h5c, wkup_detector_filter_q_fpv[4:4], dut.u_reg.regen_qs, 'h8, 3))
- `ASSERT(wkup_detector4_filter4_rd_A, rd_P(7'h5c, wkup_detector_filter_q_fpv[4:4], 'h8, 3))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector4_miodio4_wr_A, wr_P(7'h5c, wkup_detector_miodio_q_fpv[4:4], dut.u_reg.regen_qs, 'h10, 4))
- `ASSERT(wkup_detector4_miodio4_rd_A, rd_P(7'h5c, wkup_detector_miodio_q_fpv[4:4], 'h10, 4))
- // assertions for register: wkup_detector5
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector5_mode5_wr_A, wr_P(7'h60, wkup_detector_mode_q_fpv[17:15], dut.u_reg.regen_qs, 'h7, 0))
- `ASSERT(wkup_detector5_mode5_rd_A, rd_P(7'h60, wkup_detector_mode_q_fpv[17:15], 'h7, 0))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector5_filter5_wr_A, wr_P(7'h60, wkup_detector_filter_q_fpv[5:5], dut.u_reg.regen_qs, 'h8, 3))
- `ASSERT(wkup_detector5_filter5_rd_A, rd_P(7'h60, wkup_detector_filter_q_fpv[5:5], 'h8, 3))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector5_miodio5_wr_A, wr_P(7'h60, wkup_detector_miodio_q_fpv[5:5], dut.u_reg.regen_qs, 'h10, 4))
- `ASSERT(wkup_detector5_miodio5_rd_A, rd_P(7'h60, wkup_detector_miodio_q_fpv[5:5], 'h10, 4))
- // assertions for register: wkup_detector6
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector6_mode6_wr_A, wr_P(7'h64, wkup_detector_mode_q_fpv[20:18], dut.u_reg.regen_qs, 'h7, 0))
- `ASSERT(wkup_detector6_mode6_rd_A, rd_P(7'h64, wkup_detector_mode_q_fpv[20:18], 'h7, 0))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector6_filter6_wr_A, wr_P(7'h64, wkup_detector_filter_q_fpv[6:6], dut.u_reg.regen_qs, 'h8, 3))
- `ASSERT(wkup_detector6_filter6_rd_A, rd_P(7'h64, wkup_detector_filter_q_fpv[6:6], 'h8, 3))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector6_miodio6_wr_A, wr_P(7'h64, wkup_detector_miodio_q_fpv[6:6], dut.u_reg.regen_qs, 'h10, 4))
- `ASSERT(wkup_detector6_miodio6_rd_A, rd_P(7'h64, wkup_detector_miodio_q_fpv[6:6], 'h10, 4))
- // assertions for register: wkup_detector7
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector7_mode7_wr_A, wr_P(7'h68, wkup_detector_mode_q_fpv[23:21], dut.u_reg.regen_qs, 'h7, 0))
- `ASSERT(wkup_detector7_mode7_rd_A, rd_P(7'h68, wkup_detector_mode_q_fpv[23:21], 'h7, 0))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector7_filter7_wr_A, wr_P(7'h68, wkup_detector_filter_q_fpv[7:7], dut.u_reg.regen_qs, 'h8, 3))
- `ASSERT(wkup_detector7_filter7_rd_A, rd_P(7'h68, wkup_detector_filter_q_fpv[7:7], 'h8, 3))
- // this is a non-homog multi-reg
- `ASSERT(wkup_detector7_miodio7_wr_A, wr_P(7'h68, wkup_detector_miodio_q_fpv[7:7], dut.u_reg.regen_qs, 'h10, 4))
- `ASSERT(wkup_detector7_miodio7_rd_A, rd_P(7'h68, wkup_detector_miodio_q_fpv[7:7], 'h10, 4))
-
- // define local fpv variable for multi-reg
- logic [63:0] wkup_detector_cnt_th_q_fpv;
- for (genvar s = 0; s < 8; s++) begin : gen_wkup_detector_cnt_th_q
- assign wkup_detector_cnt_th_q_fpv[((s+1)*8-1):s*8] = reg2hw.wkup_detector_cnt_th[s].q;
- end
-
- // assertions for register: wkup_detector_cnt_th0
- `ASSERT(wkup_detector_cnt_th0_wr_A, wr_P(7'h6c, wkup_detector_cnt_th_q_fpv[31:0], dut.u_reg.regen_qs, 'hffffffff, 0))
- `ASSERT(wkup_detector_cnt_th0_rd_A, rd_P(7'h6c, wkup_detector_cnt_th_q_fpv[31:0], 'hffffffff, 0))
- // assertions for register: wkup_detector_cnt_th1
- `ASSERT(wkup_detector_cnt_th1_wr_A, wr_P(7'h70, wkup_detector_cnt_th_q_fpv[63:32], dut.u_reg.regen_qs, 'hffffffff, 0))
- `ASSERT(wkup_detector_cnt_th1_rd_A, rd_P(7'h70, wkup_detector_cnt_th_q_fpv[63:32], 'hffffffff, 0))
-
- // define local fpv variable for multi-reg
- logic [39:0] wkup_detector_padsel_q_fpv;
- for (genvar s = 0; s < 8; s++) begin : gen_wkup_detector_padsel_q
- assign wkup_detector_padsel_q_fpv[((s+1)*5-1):s*5] = reg2hw.wkup_detector_padsel[s].q;
- end
-
- // assertions for register: wkup_detector_padsel0
- `ASSERT(wkup_detector_padsel0_wr_A, wr_P(7'h74, wkup_detector_padsel_q_fpv[29:0], dut.u_reg.regen_qs, 'h3fffffff, 0))
- `ASSERT(wkup_detector_padsel0_rd_A, rd_P(7'h74, wkup_detector_padsel_q_fpv[29:0], 'h3fffffff, 0))
- // assertions for register: wkup_detector_padsel1
- `ASSERT(wkup_detector_padsel1_wr_A, wr_P(7'h78, wkup_detector_padsel_q_fpv[39:30], dut.u_reg.regen_qs, 'h3ff, 0))
- `ASSERT(wkup_detector_padsel1_rd_A, rd_P(7'h78, wkup_detector_padsel_q_fpv[39:30], 'h3ff, 0))
-
- // define local fpv variable for multi-reg
- logic [7:0] wkup_cause_q_fpv;
- logic [7:0] wkup_cause_d_fpv;
- for (genvar s = 0; s < 8; s++) begin : gen_wkup_cause_q
- assign wkup_cause_q_fpv[((s+1)*1-1):s*1] = reg2hw.wkup_cause[s].q;
- assign wkup_cause_d_fpv[((s+1)*1-1):s*1] = hw2reg.wkup_cause[s].d;
- end
-
- // assertions for register: wkup_cause
- `ASSERT(wkup_cause_wr_A, wr_ext_P(7'h7c, wkup_cause_q_fpv[7:0], dut.u_reg.regen_qs, 'hff, 0))
- `ASSERT(wkup_cause_rd_A, rd_ext_P(7'h7c, wkup_cause_d_fpv[7:0], 'hff, 0))
-
-
-endmodule
diff --git a/hw/ip/rv_plic/data/rv_plic_fpv.core.tpl b/hw/ip/rv_plic/data/rv_plic_fpv.core.tpl
index fd5c59f..507e02d 100644
--- a/hw/ip/rv_plic/data/rv_plic_fpv.core.tpl
+++ b/hw/ip/rv_plic/data/rv_plic_fpv.core.tpl
@@ -10,12 +10,19 @@
depend:
- lowrisc:fpv:rv_plic_component_fpv
- lowrisc:top_earlgrey:rv_plic
+ - lowrisc:fpv:csr_assert_gen
files:
- - rv_plic_csr_assert_fpv.sv
- rv_plic_bind_fpv.sv
- rv_plic_fpv.sv
file_type: systemVerilogSource
+generate:
+ csr_assert_gen:
+ generator: csr_assert_gen
+ parameters:
+ spec: ../../data/autogen/rv_plic.hjson
+ depend: lowrisc:top_earlgrey:rv_plic
+
targets:
default: &default_target
# note, this setting is just used
@@ -23,6 +30,8 @@
default_tool: icarus
filesets:
- files_formal
+ generate:
+ - csr_assert_gen
toplevel: rv_plic_fpv
formal:
diff --git a/hw/ip/rv_plic/fpv/rv_plic_generic_fpv.core b/hw/ip/rv_plic/fpv/rv_plic_generic_fpv.core
index 0f98a47..305b989 100644
--- a/hw/ip/rv_plic/fpv/rv_plic_generic_fpv.core
+++ b/hw/ip/rv_plic/fpv/rv_plic_generic_fpv.core
@@ -12,12 +12,19 @@
# note: this is an example config which may differ
# from a particular top-level config
- lowrisc:ip:rv_plic_example
+ - lowrisc:fpv:csr_assert_gen
files:
- - vip/rv_plic_csr_assert_fpv.sv
- tb/rv_plic_bind_fpv.sv
- tb/rv_plic_generic_fpv.sv
file_type: systemVerilogSource
+generate:
+ csr_assert_gen:
+ generator: csr_assert_gen
+ parameters:
+ spec: ../data/rv_plic.hjson
+ depend: lowrisc:ip:rv_plic_example
+
targets:
default: &default_target
# note, this setting is just used
@@ -25,6 +32,8 @@
default_tool: icarus
filesets:
- files_formal
+ generate:
+ - csr_assert_gen
toplevel: rv_plic_generic_fpv
formal:
diff --git a/hw/ip/rv_plic/fpv/vip/rv_plic_csr_assert_fpv.sv b/hw/ip/rv_plic/fpv/vip/rv_plic_csr_assert_fpv.sv
deleted file mode 100644
index d9e1574..0000000
--- a/hw/ip/rv_plic/fpv/vip/rv_plic_csr_assert_fpv.sv
+++ /dev/null
@@ -1,285 +0,0 @@
-// 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 and regwen reg
-// This automation assumes that W1C and W0C are registers with 1 bit per field
-
-`include "prim_assert.sv"
-
-// Block: rv_plic
-module rv_plic_csr_assert_fpv import tlul_pkg::*; import rv_plic_reg_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 rv_plic_reg2hw_t reg2hw,
- input rv_plic_hw2reg_t hw2reg
-);
-
- 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;
-
- // declare common read and write sequences
- sequence device_wr_S(logic [8: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 [8: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
- // 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 [8:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- 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 << lsb) == exp_data || !regen);
- endproperty
-
- // external reg will use one clk cycle to update act_data from external
- property wr_ext_P(bit [8:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- 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) << lsb) == exp_data || !regen);
- endproperty
-
- property w1c_P(bit [8:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- logic [DWidth-1:0] id, exp_data;
- (device_wr_S(addr), id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask & '0) ##1
- first_match(##[0:$] d2h.d_valid && d2h.d_source == id) |->
- (d2h.d_error || (act_data << lsb) == exp_data || !regen);
- endproperty
-
- property w1c_ext_P(bit [8:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- logic [DWidth-1:0] id, exp_data;
- (device_wr_S(addr), id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask & '0) ##1
- first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
- (d2h.d_error || ($past(act_data) << lsb) == exp_data || !regen);
- endproperty
-
- property rd_P(bit [8:0] addr, bit [DWidth-1:0] act_data, bit [DWidth-1:0] mask, int lsb);
- 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 & mask) >> lsb == exp_data);
- endproperty
-
- property rd_ext_P(bit [8:0] addr, bit [DWidth-1:0] act_data, bit [DWidth-1:0] mask,
- int lsb);
- 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 & mask) >> lsb == exp_data);
- endproperty
-
- // read a WO register, always return 0
- property r_wo_P(bit [8: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
-
- // TODO: currently not used, will use once support regwen reg
- property wr_regen_stable_P(bit regen, bit [DWidth-1:0] exp_data);
- (!regen && $stable(regen)) |-> $stable(exp_data);
- endproperty
-
-
- // define local fpv variable for multi-reg
- logic [31:0] ip_d_fpv;
- for (genvar s = 0; s < 32; s++) begin : gen_ip_q
- assign ip_d_fpv[((s+1)*1-1):s*1] = hw2reg.ip[s].d;
- end
-
- // assertions for register: ip
- `ASSERT(ip_rd_A, rd_P(9'h0, ip_d_fpv[31:0], 'hffffffff, 0))
-
- // define local fpv variable for multi-reg
- logic [31:0] le_q_fpv;
- for (genvar s = 0; s < 32; s++) begin : gen_le_q
- assign le_q_fpv[((s+1)*1-1):s*1] = reg2hw.le[s].q;
- end
-
- // assertions for register: le
- `ASSERT(le_wr_A, wr_P(9'h4, le_q_fpv[31:0], 1, 'hffffffff, 0))
- `ASSERT(le_rd_A, rd_P(9'h4, le_q_fpv[31:0], 'hffffffff, 0))
-
- // assertions for register: prio0
- `ASSERT(prio0_wr_A, wr_P(9'h8, reg2hw.prio0.q, 1, 'h7, 0))
- `ASSERT(prio0_rd_A, rd_P(9'h8, reg2hw.prio0.q, 'hffffffff, 0))
-
- // assertions for register: prio1
- `ASSERT(prio1_wr_A, wr_P(9'hc, reg2hw.prio1.q, 1, 'h7, 0))
- `ASSERT(prio1_rd_A, rd_P(9'hc, reg2hw.prio1.q, 'hffffffff, 0))
-
- // assertions for register: prio2
- `ASSERT(prio2_wr_A, wr_P(9'h10, reg2hw.prio2.q, 1, 'h7, 0))
- `ASSERT(prio2_rd_A, rd_P(9'h10, reg2hw.prio2.q, 'hffffffff, 0))
-
- // assertions for register: prio3
- `ASSERT(prio3_wr_A, wr_P(9'h14, reg2hw.prio3.q, 1, 'h7, 0))
- `ASSERT(prio3_rd_A, rd_P(9'h14, reg2hw.prio3.q, 'hffffffff, 0))
-
- // assertions for register: prio4
- `ASSERT(prio4_wr_A, wr_P(9'h18, reg2hw.prio4.q, 1, 'h7, 0))
- `ASSERT(prio4_rd_A, rd_P(9'h18, reg2hw.prio4.q, 'hffffffff, 0))
-
- // assertions for register: prio5
- `ASSERT(prio5_wr_A, wr_P(9'h1c, reg2hw.prio5.q, 1, 'h7, 0))
- `ASSERT(prio5_rd_A, rd_P(9'h1c, reg2hw.prio5.q, 'hffffffff, 0))
-
- // assertions for register: prio6
- `ASSERT(prio6_wr_A, wr_P(9'h20, reg2hw.prio6.q, 1, 'h7, 0))
- `ASSERT(prio6_rd_A, rd_P(9'h20, reg2hw.prio6.q, 'hffffffff, 0))
-
- // assertions for register: prio7
- `ASSERT(prio7_wr_A, wr_P(9'h24, reg2hw.prio7.q, 1, 'h7, 0))
- `ASSERT(prio7_rd_A, rd_P(9'h24, reg2hw.prio7.q, 'hffffffff, 0))
-
- // assertions for register: prio8
- `ASSERT(prio8_wr_A, wr_P(9'h28, reg2hw.prio8.q, 1, 'h7, 0))
- `ASSERT(prio8_rd_A, rd_P(9'h28, reg2hw.prio8.q, 'hffffffff, 0))
-
- // assertions for register: prio9
- `ASSERT(prio9_wr_A, wr_P(9'h2c, reg2hw.prio9.q, 1, 'h7, 0))
- `ASSERT(prio9_rd_A, rd_P(9'h2c, reg2hw.prio9.q, 'hffffffff, 0))
-
- // assertions for register: prio10
- `ASSERT(prio10_wr_A, wr_P(9'h30, reg2hw.prio10.q, 1, 'h7, 0))
- `ASSERT(prio10_rd_A, rd_P(9'h30, reg2hw.prio10.q, 'hffffffff, 0))
-
- // assertions for register: prio11
- `ASSERT(prio11_wr_A, wr_P(9'h34, reg2hw.prio11.q, 1, 'h7, 0))
- `ASSERT(prio11_rd_A, rd_P(9'h34, reg2hw.prio11.q, 'hffffffff, 0))
-
- // assertions for register: prio12
- `ASSERT(prio12_wr_A, wr_P(9'h38, reg2hw.prio12.q, 1, 'h7, 0))
- `ASSERT(prio12_rd_A, rd_P(9'h38, reg2hw.prio12.q, 'hffffffff, 0))
-
- // assertions for register: prio13
- `ASSERT(prio13_wr_A, wr_P(9'h3c, reg2hw.prio13.q, 1, 'h7, 0))
- `ASSERT(prio13_rd_A, rd_P(9'h3c, reg2hw.prio13.q, 'hffffffff, 0))
-
- // assertions for register: prio14
- `ASSERT(prio14_wr_A, wr_P(9'h40, reg2hw.prio14.q, 1, 'h7, 0))
- `ASSERT(prio14_rd_A, rd_P(9'h40, reg2hw.prio14.q, 'hffffffff, 0))
-
- // assertions for register: prio15
- `ASSERT(prio15_wr_A, wr_P(9'h44, reg2hw.prio15.q, 1, 'h7, 0))
- `ASSERT(prio15_rd_A, rd_P(9'h44, reg2hw.prio15.q, 'hffffffff, 0))
-
- // assertions for register: prio16
- `ASSERT(prio16_wr_A, wr_P(9'h48, reg2hw.prio16.q, 1, 'h7, 0))
- `ASSERT(prio16_rd_A, rd_P(9'h48, reg2hw.prio16.q, 'hffffffff, 0))
-
- // assertions for register: prio17
- `ASSERT(prio17_wr_A, wr_P(9'h4c, reg2hw.prio17.q, 1, 'h7, 0))
- `ASSERT(prio17_rd_A, rd_P(9'h4c, reg2hw.prio17.q, 'hffffffff, 0))
-
- // assertions for register: prio18
- `ASSERT(prio18_wr_A, wr_P(9'h50, reg2hw.prio18.q, 1, 'h7, 0))
- `ASSERT(prio18_rd_A, rd_P(9'h50, reg2hw.prio18.q, 'hffffffff, 0))
-
- // assertions for register: prio19
- `ASSERT(prio19_wr_A, wr_P(9'h54, reg2hw.prio19.q, 1, 'h7, 0))
- `ASSERT(prio19_rd_A, rd_P(9'h54, reg2hw.prio19.q, 'hffffffff, 0))
-
- // assertions for register: prio20
- `ASSERT(prio20_wr_A, wr_P(9'h58, reg2hw.prio20.q, 1, 'h7, 0))
- `ASSERT(prio20_rd_A, rd_P(9'h58, reg2hw.prio20.q, 'hffffffff, 0))
-
- // assertions for register: prio21
- `ASSERT(prio21_wr_A, wr_P(9'h5c, reg2hw.prio21.q, 1, 'h7, 0))
- `ASSERT(prio21_rd_A, rd_P(9'h5c, reg2hw.prio21.q, 'hffffffff, 0))
-
- // assertions for register: prio22
- `ASSERT(prio22_wr_A, wr_P(9'h60, reg2hw.prio22.q, 1, 'h7, 0))
- `ASSERT(prio22_rd_A, rd_P(9'h60, reg2hw.prio22.q, 'hffffffff, 0))
-
- // assertions for register: prio23
- `ASSERT(prio23_wr_A, wr_P(9'h64, reg2hw.prio23.q, 1, 'h7, 0))
- `ASSERT(prio23_rd_A, rd_P(9'h64, reg2hw.prio23.q, 'hffffffff, 0))
-
- // assertions for register: prio24
- `ASSERT(prio24_wr_A, wr_P(9'h68, reg2hw.prio24.q, 1, 'h7, 0))
- `ASSERT(prio24_rd_A, rd_P(9'h68, reg2hw.prio24.q, 'hffffffff, 0))
-
- // assertions for register: prio25
- `ASSERT(prio25_wr_A, wr_P(9'h6c, reg2hw.prio25.q, 1, 'h7, 0))
- `ASSERT(prio25_rd_A, rd_P(9'h6c, reg2hw.prio25.q, 'hffffffff, 0))
-
- // assertions for register: prio26
- `ASSERT(prio26_wr_A, wr_P(9'h70, reg2hw.prio26.q, 1, 'h7, 0))
- `ASSERT(prio26_rd_A, rd_P(9'h70, reg2hw.prio26.q, 'hffffffff, 0))
-
- // assertions for register: prio27
- `ASSERT(prio27_wr_A, wr_P(9'h74, reg2hw.prio27.q, 1, 'h7, 0))
- `ASSERT(prio27_rd_A, rd_P(9'h74, reg2hw.prio27.q, 'hffffffff, 0))
-
- // assertions for register: prio28
- `ASSERT(prio28_wr_A, wr_P(9'h78, reg2hw.prio28.q, 1, 'h7, 0))
- `ASSERT(prio28_rd_A, rd_P(9'h78, reg2hw.prio28.q, 'hffffffff, 0))
-
- // assertions for register: prio29
- `ASSERT(prio29_wr_A, wr_P(9'h7c, reg2hw.prio29.q, 1, 'h7, 0))
- `ASSERT(prio29_rd_A, rd_P(9'h7c, reg2hw.prio29.q, 'hffffffff, 0))
-
- // assertions for register: prio30
- `ASSERT(prio30_wr_A, wr_P(9'h80, reg2hw.prio30.q, 1, 'h7, 0))
- `ASSERT(prio30_rd_A, rd_P(9'h80, reg2hw.prio30.q, 'hffffffff, 0))
-
- // assertions for register: prio31
- `ASSERT(prio31_wr_A, wr_P(9'h84, reg2hw.prio31.q, 1, 'h7, 0))
- `ASSERT(prio31_rd_A, rd_P(9'h84, reg2hw.prio31.q, 'hffffffff, 0))
-
- // define local fpv variable for multi-reg
- logic [31:0] ie0_q_fpv;
- for (genvar s = 0; s < 32; s++) begin : gen_ie0_q
- assign ie0_q_fpv[((s+1)*1-1):s*1] = reg2hw.ie0[s].q;
- end
-
- // assertions for register: ie0
- `ASSERT(ie0_wr_A, wr_P(9'h100, ie0_q_fpv[31:0], 1, 'hffffffff, 0))
- `ASSERT(ie0_rd_A, rd_P(9'h100, ie0_q_fpv[31:0], 'hffffffff, 0))
-
- // assertions for register: threshold0
- `ASSERT(threshold0_wr_A, wr_P(9'h104, reg2hw.threshold0.q, 1, 'h7, 0))
- `ASSERT(threshold0_rd_A, rd_P(9'h104, reg2hw.threshold0.q, 'hffffffff, 0))
-
- // assertions for register: cc0
- `ASSERT(cc0_wr_A, wr_ext_P(9'h108, reg2hw.cc0.q, 1, 'h3f, 0))
- `ASSERT(cc0_rd_A, rd_ext_P(9'h108, hw2reg.cc0.d, 'hffffffff, 0))
-
- // assertions for register: msip0
- `ASSERT(msip0_wr_A, wr_P(9'h10c, reg2hw.msip0.q, 1, 'h1, 0))
- `ASSERT(msip0_rd_A, rd_P(9'h10c, reg2hw.msip0.q, 'hffffffff, 0))
-
-
-endmodule
diff --git a/hw/top_earlgrey/ip/rv_plic/fpv/autogen/rv_plic_csr_assert_fpv.sv b/hw/top_earlgrey/ip/rv_plic/fpv/autogen/rv_plic_csr_assert_fpv.sv
deleted file mode 100644
index 67aa2a3..0000000
--- a/hw/top_earlgrey/ip/rv_plic/fpv/autogen/rv_plic_csr_assert_fpv.sv
+++ /dev/null
@@ -1,505 +0,0 @@
-// 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 and regwen reg
-// This automation assumes that W1C and W0C are registers with 1 bit per field
-
-`include "prim_assert.sv"
-
-// Block: rv_plic
-module rv_plic_csr_assert_fpv import tlul_pkg::*; import rv_plic_reg_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 rv_plic_reg2hw_t reg2hw,
- input rv_plic_hw2reg_t hw2reg
-);
-
- 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;
-
- // declare common read and write sequences
- sequence device_wr_S(logic [9: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 [9: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
- // 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 [9:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- 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 << lsb) == exp_data || !regen);
- endproperty
-
- // external reg will use one clk cycle to update act_data from external
- property wr_ext_P(bit [9:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- 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) << lsb) == exp_data || !regen);
- endproperty
-
- property w1c_P(bit [9:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- logic [DWidth-1:0] id, exp_data;
- (device_wr_S(addr), id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask & '0) ##1
- first_match(##[0:$] d2h.d_valid && d2h.d_source == id) |->
- (d2h.d_error || (act_data << lsb) == exp_data || !regen);
- endproperty
-
- property w1c_ext_P(bit [9:0] addr, bit [DWidth-1:0] act_data, bit regen,
- bit [DWidth-1:0] mask, int lsb);
- logic [DWidth-1:0] id, exp_data;
- (device_wr_S(addr), id = h2d.a_source, exp_data = h2d.a_data & a_mask_bit & mask & '0) ##1
- first_match(##[0:$] (d2h.d_valid && d2h.d_source == id)) |->
- (d2h.d_error || ($past(act_data) << lsb) == exp_data || !regen);
- endproperty
-
- property rd_P(bit [9:0] addr, bit [DWidth-1:0] act_data, bit [DWidth-1:0] mask, int lsb);
- 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 & mask) >> lsb == exp_data);
- endproperty
-
- property rd_ext_P(bit [9:0] addr, bit [DWidth-1:0] act_data, bit [DWidth-1:0] mask,
- int lsb);
- 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 & mask) >> lsb == exp_data);
- endproperty
-
- // read a WO register, always return 0
- property r_wo_P(bit [9: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
-
- // TODO: currently not used, will use once support regwen reg
- property wr_regen_stable_P(bit regen, bit [DWidth-1:0] exp_data);
- (!regen && $stable(regen)) |-> $stable(exp_data);
- endproperty
-
-
- // define local fpv variable for multi-reg
- logic [82:0] ip_d_fpv;
- for (genvar s = 0; s < 83; s++) begin : gen_ip_q
- assign ip_d_fpv[((s+1)*1-1):s*1] = hw2reg.ip[s].d;
- end
-
- // assertions for register: ip0
- `ASSERT(ip0_rd_A, rd_P(10'h0, ip_d_fpv[31:0], 'hffffffff, 0))
- // assertions for register: ip1
- `ASSERT(ip1_rd_A, rd_P(10'h4, ip_d_fpv[63:32], 'hffffffff, 0))
- // assertions for register: ip2
- `ASSERT(ip2_rd_A, rd_P(10'h8, ip_d_fpv[82:64], 'h7ffff, 0))
-
- // define local fpv variable for multi-reg
- logic [82:0] le_q_fpv;
- for (genvar s = 0; s < 83; s++) begin : gen_le_q
- assign le_q_fpv[((s+1)*1-1):s*1] = reg2hw.le[s].q;
- end
-
- // assertions for register: le0
- `ASSERT(le0_wr_A, wr_P(10'hc, le_q_fpv[31:0], 1, 'hffffffff, 0))
- `ASSERT(le0_rd_A, rd_P(10'hc, le_q_fpv[31:0], 'hffffffff, 0))
- // assertions for register: le1
- `ASSERT(le1_wr_A, wr_P(10'h10, le_q_fpv[63:32], 1, 'hffffffff, 0))
- `ASSERT(le1_rd_A, rd_P(10'h10, le_q_fpv[63:32], 'hffffffff, 0))
- // assertions for register: le2
- `ASSERT(le2_wr_A, wr_P(10'h14, le_q_fpv[82:64], 1, 'h7ffff, 0))
- `ASSERT(le2_rd_A, rd_P(10'h14, le_q_fpv[82:64], 'h7ffff, 0))
-
- // assertions for register: prio0
- `ASSERT(prio0_wr_A, wr_P(10'h18, reg2hw.prio0.q, 1, 'h3, 0))
- `ASSERT(prio0_rd_A, rd_P(10'h18, reg2hw.prio0.q, 'hffffffff, 0))
-
- // assertions for register: prio1
- `ASSERT(prio1_wr_A, wr_P(10'h1c, reg2hw.prio1.q, 1, 'h3, 0))
- `ASSERT(prio1_rd_A, rd_P(10'h1c, reg2hw.prio1.q, 'hffffffff, 0))
-
- // assertions for register: prio2
- `ASSERT(prio2_wr_A, wr_P(10'h20, reg2hw.prio2.q, 1, 'h3, 0))
- `ASSERT(prio2_rd_A, rd_P(10'h20, reg2hw.prio2.q, 'hffffffff, 0))
-
- // assertions for register: prio3
- `ASSERT(prio3_wr_A, wr_P(10'h24, reg2hw.prio3.q, 1, 'h3, 0))
- `ASSERT(prio3_rd_A, rd_P(10'h24, reg2hw.prio3.q, 'hffffffff, 0))
-
- // assertions for register: prio4
- `ASSERT(prio4_wr_A, wr_P(10'h28, reg2hw.prio4.q, 1, 'h3, 0))
- `ASSERT(prio4_rd_A, rd_P(10'h28, reg2hw.prio4.q, 'hffffffff, 0))
-
- // assertions for register: prio5
- `ASSERT(prio5_wr_A, wr_P(10'h2c, reg2hw.prio5.q, 1, 'h3, 0))
- `ASSERT(prio5_rd_A, rd_P(10'h2c, reg2hw.prio5.q, 'hffffffff, 0))
-
- // assertions for register: prio6
- `ASSERT(prio6_wr_A, wr_P(10'h30, reg2hw.prio6.q, 1, 'h3, 0))
- `ASSERT(prio6_rd_A, rd_P(10'h30, reg2hw.prio6.q, 'hffffffff, 0))
-
- // assertions for register: prio7
- `ASSERT(prio7_wr_A, wr_P(10'h34, reg2hw.prio7.q, 1, 'h3, 0))
- `ASSERT(prio7_rd_A, rd_P(10'h34, reg2hw.prio7.q, 'hffffffff, 0))
-
- // assertions for register: prio8
- `ASSERT(prio8_wr_A, wr_P(10'h38, reg2hw.prio8.q, 1, 'h3, 0))
- `ASSERT(prio8_rd_A, rd_P(10'h38, reg2hw.prio8.q, 'hffffffff, 0))
-
- // assertions for register: prio9
- `ASSERT(prio9_wr_A, wr_P(10'h3c, reg2hw.prio9.q, 1, 'h3, 0))
- `ASSERT(prio9_rd_A, rd_P(10'h3c, reg2hw.prio9.q, 'hffffffff, 0))
-
- // assertions for register: prio10
- `ASSERT(prio10_wr_A, wr_P(10'h40, reg2hw.prio10.q, 1, 'h3, 0))
- `ASSERT(prio10_rd_A, rd_P(10'h40, reg2hw.prio10.q, 'hffffffff, 0))
-
- // assertions for register: prio11
- `ASSERT(prio11_wr_A, wr_P(10'h44, reg2hw.prio11.q, 1, 'h3, 0))
- `ASSERT(prio11_rd_A, rd_P(10'h44, reg2hw.prio11.q, 'hffffffff, 0))
-
- // assertions for register: prio12
- `ASSERT(prio12_wr_A, wr_P(10'h48, reg2hw.prio12.q, 1, 'h3, 0))
- `ASSERT(prio12_rd_A, rd_P(10'h48, reg2hw.prio12.q, 'hffffffff, 0))
-
- // assertions for register: prio13
- `ASSERT(prio13_wr_A, wr_P(10'h4c, reg2hw.prio13.q, 1, 'h3, 0))
- `ASSERT(prio13_rd_A, rd_P(10'h4c, reg2hw.prio13.q, 'hffffffff, 0))
-
- // assertions for register: prio14
- `ASSERT(prio14_wr_A, wr_P(10'h50, reg2hw.prio14.q, 1, 'h3, 0))
- `ASSERT(prio14_rd_A, rd_P(10'h50, reg2hw.prio14.q, 'hffffffff, 0))
-
- // assertions for register: prio15
- `ASSERT(prio15_wr_A, wr_P(10'h54, reg2hw.prio15.q, 1, 'h3, 0))
- `ASSERT(prio15_rd_A, rd_P(10'h54, reg2hw.prio15.q, 'hffffffff, 0))
-
- // assertions for register: prio16
- `ASSERT(prio16_wr_A, wr_P(10'h58, reg2hw.prio16.q, 1, 'h3, 0))
- `ASSERT(prio16_rd_A, rd_P(10'h58, reg2hw.prio16.q, 'hffffffff, 0))
-
- // assertions for register: prio17
- `ASSERT(prio17_wr_A, wr_P(10'h5c, reg2hw.prio17.q, 1, 'h3, 0))
- `ASSERT(prio17_rd_A, rd_P(10'h5c, reg2hw.prio17.q, 'hffffffff, 0))
-
- // assertions for register: prio18
- `ASSERT(prio18_wr_A, wr_P(10'h60, reg2hw.prio18.q, 1, 'h3, 0))
- `ASSERT(prio18_rd_A, rd_P(10'h60, reg2hw.prio18.q, 'hffffffff, 0))
-
- // assertions for register: prio19
- `ASSERT(prio19_wr_A, wr_P(10'h64, reg2hw.prio19.q, 1, 'h3, 0))
- `ASSERT(prio19_rd_A, rd_P(10'h64, reg2hw.prio19.q, 'hffffffff, 0))
-
- // assertions for register: prio20
- `ASSERT(prio20_wr_A, wr_P(10'h68, reg2hw.prio20.q, 1, 'h3, 0))
- `ASSERT(prio20_rd_A, rd_P(10'h68, reg2hw.prio20.q, 'hffffffff, 0))
-
- // assertions for register: prio21
- `ASSERT(prio21_wr_A, wr_P(10'h6c, reg2hw.prio21.q, 1, 'h3, 0))
- `ASSERT(prio21_rd_A, rd_P(10'h6c, reg2hw.prio21.q, 'hffffffff, 0))
-
- // assertions for register: prio22
- `ASSERT(prio22_wr_A, wr_P(10'h70, reg2hw.prio22.q, 1, 'h3, 0))
- `ASSERT(prio22_rd_A, rd_P(10'h70, reg2hw.prio22.q, 'hffffffff, 0))
-
- // assertions for register: prio23
- `ASSERT(prio23_wr_A, wr_P(10'h74, reg2hw.prio23.q, 1, 'h3, 0))
- `ASSERT(prio23_rd_A, rd_P(10'h74, reg2hw.prio23.q, 'hffffffff, 0))
-
- // assertions for register: prio24
- `ASSERT(prio24_wr_A, wr_P(10'h78, reg2hw.prio24.q, 1, 'h3, 0))
- `ASSERT(prio24_rd_A, rd_P(10'h78, reg2hw.prio24.q, 'hffffffff, 0))
-
- // assertions for register: prio25
- `ASSERT(prio25_wr_A, wr_P(10'h7c, reg2hw.prio25.q, 1, 'h3, 0))
- `ASSERT(prio25_rd_A, rd_P(10'h7c, reg2hw.prio25.q, 'hffffffff, 0))
-
- // assertions for register: prio26
- `ASSERT(prio26_wr_A, wr_P(10'h80, reg2hw.prio26.q, 1, 'h3, 0))
- `ASSERT(prio26_rd_A, rd_P(10'h80, reg2hw.prio26.q, 'hffffffff, 0))
-
- // assertions for register: prio27
- `ASSERT(prio27_wr_A, wr_P(10'h84, reg2hw.prio27.q, 1, 'h3, 0))
- `ASSERT(prio27_rd_A, rd_P(10'h84, reg2hw.prio27.q, 'hffffffff, 0))
-
- // assertions for register: prio28
- `ASSERT(prio28_wr_A, wr_P(10'h88, reg2hw.prio28.q, 1, 'h3, 0))
- `ASSERT(prio28_rd_A, rd_P(10'h88, reg2hw.prio28.q, 'hffffffff, 0))
-
- // assertions for register: prio29
- `ASSERT(prio29_wr_A, wr_P(10'h8c, reg2hw.prio29.q, 1, 'h3, 0))
- `ASSERT(prio29_rd_A, rd_P(10'h8c, reg2hw.prio29.q, 'hffffffff, 0))
-
- // assertions for register: prio30
- `ASSERT(prio30_wr_A, wr_P(10'h90, reg2hw.prio30.q, 1, 'h3, 0))
- `ASSERT(prio30_rd_A, rd_P(10'h90, reg2hw.prio30.q, 'hffffffff, 0))
-
- // assertions for register: prio31
- `ASSERT(prio31_wr_A, wr_P(10'h94, reg2hw.prio31.q, 1, 'h3, 0))
- `ASSERT(prio31_rd_A, rd_P(10'h94, reg2hw.prio31.q, 'hffffffff, 0))
-
- // assertions for register: prio32
- `ASSERT(prio32_wr_A, wr_P(10'h98, reg2hw.prio32.q, 1, 'h3, 0))
- `ASSERT(prio32_rd_A, rd_P(10'h98, reg2hw.prio32.q, 'hffffffff, 0))
-
- // assertions for register: prio33
- `ASSERT(prio33_wr_A, wr_P(10'h9c, reg2hw.prio33.q, 1, 'h3, 0))
- `ASSERT(prio33_rd_A, rd_P(10'h9c, reg2hw.prio33.q, 'hffffffff, 0))
-
- // assertions for register: prio34
- `ASSERT(prio34_wr_A, wr_P(10'ha0, reg2hw.prio34.q, 1, 'h3, 0))
- `ASSERT(prio34_rd_A, rd_P(10'ha0, reg2hw.prio34.q, 'hffffffff, 0))
-
- // assertions for register: prio35
- `ASSERT(prio35_wr_A, wr_P(10'ha4, reg2hw.prio35.q, 1, 'h3, 0))
- `ASSERT(prio35_rd_A, rd_P(10'ha4, reg2hw.prio35.q, 'hffffffff, 0))
-
- // assertions for register: prio36
- `ASSERT(prio36_wr_A, wr_P(10'ha8, reg2hw.prio36.q, 1, 'h3, 0))
- `ASSERT(prio36_rd_A, rd_P(10'ha8, reg2hw.prio36.q, 'hffffffff, 0))
-
- // assertions for register: prio37
- `ASSERT(prio37_wr_A, wr_P(10'hac, reg2hw.prio37.q, 1, 'h3, 0))
- `ASSERT(prio37_rd_A, rd_P(10'hac, reg2hw.prio37.q, 'hffffffff, 0))
-
- // assertions for register: prio38
- `ASSERT(prio38_wr_A, wr_P(10'hb0, reg2hw.prio38.q, 1, 'h3, 0))
- `ASSERT(prio38_rd_A, rd_P(10'hb0, reg2hw.prio38.q, 'hffffffff, 0))
-
- // assertions for register: prio39
- `ASSERT(prio39_wr_A, wr_P(10'hb4, reg2hw.prio39.q, 1, 'h3, 0))
- `ASSERT(prio39_rd_A, rd_P(10'hb4, reg2hw.prio39.q, 'hffffffff, 0))
-
- // assertions for register: prio40
- `ASSERT(prio40_wr_A, wr_P(10'hb8, reg2hw.prio40.q, 1, 'h3, 0))
- `ASSERT(prio40_rd_A, rd_P(10'hb8, reg2hw.prio40.q, 'hffffffff, 0))
-
- // assertions for register: prio41
- `ASSERT(prio41_wr_A, wr_P(10'hbc, reg2hw.prio41.q, 1, 'h3, 0))
- `ASSERT(prio41_rd_A, rd_P(10'hbc, reg2hw.prio41.q, 'hffffffff, 0))
-
- // assertions for register: prio42
- `ASSERT(prio42_wr_A, wr_P(10'hc0, reg2hw.prio42.q, 1, 'h3, 0))
- `ASSERT(prio42_rd_A, rd_P(10'hc0, reg2hw.prio42.q, 'hffffffff, 0))
-
- // assertions for register: prio43
- `ASSERT(prio43_wr_A, wr_P(10'hc4, reg2hw.prio43.q, 1, 'h3, 0))
- `ASSERT(prio43_rd_A, rd_P(10'hc4, reg2hw.prio43.q, 'hffffffff, 0))
-
- // assertions for register: prio44
- `ASSERT(prio44_wr_A, wr_P(10'hc8, reg2hw.prio44.q, 1, 'h3, 0))
- `ASSERT(prio44_rd_A, rd_P(10'hc8, reg2hw.prio44.q, 'hffffffff, 0))
-
- // assertions for register: prio45
- `ASSERT(prio45_wr_A, wr_P(10'hcc, reg2hw.prio45.q, 1, 'h3, 0))
- `ASSERT(prio45_rd_A, rd_P(10'hcc, reg2hw.prio45.q, 'hffffffff, 0))
-
- // assertions for register: prio46
- `ASSERT(prio46_wr_A, wr_P(10'hd0, reg2hw.prio46.q, 1, 'h3, 0))
- `ASSERT(prio46_rd_A, rd_P(10'hd0, reg2hw.prio46.q, 'hffffffff, 0))
-
- // assertions for register: prio47
- `ASSERT(prio47_wr_A, wr_P(10'hd4, reg2hw.prio47.q, 1, 'h3, 0))
- `ASSERT(prio47_rd_A, rd_P(10'hd4, reg2hw.prio47.q, 'hffffffff, 0))
-
- // assertions for register: prio48
- `ASSERT(prio48_wr_A, wr_P(10'hd8, reg2hw.prio48.q, 1, 'h3, 0))
- `ASSERT(prio48_rd_A, rd_P(10'hd8, reg2hw.prio48.q, 'hffffffff, 0))
-
- // assertions for register: prio49
- `ASSERT(prio49_wr_A, wr_P(10'hdc, reg2hw.prio49.q, 1, 'h3, 0))
- `ASSERT(prio49_rd_A, rd_P(10'hdc, reg2hw.prio49.q, 'hffffffff, 0))
-
- // assertions for register: prio50
- `ASSERT(prio50_wr_A, wr_P(10'he0, reg2hw.prio50.q, 1, 'h3, 0))
- `ASSERT(prio50_rd_A, rd_P(10'he0, reg2hw.prio50.q, 'hffffffff, 0))
-
- // assertions for register: prio51
- `ASSERT(prio51_wr_A, wr_P(10'he4, reg2hw.prio51.q, 1, 'h3, 0))
- `ASSERT(prio51_rd_A, rd_P(10'he4, reg2hw.prio51.q, 'hffffffff, 0))
-
- // assertions for register: prio52
- `ASSERT(prio52_wr_A, wr_P(10'he8, reg2hw.prio52.q, 1, 'h3, 0))
- `ASSERT(prio52_rd_A, rd_P(10'he8, reg2hw.prio52.q, 'hffffffff, 0))
-
- // assertions for register: prio53
- `ASSERT(prio53_wr_A, wr_P(10'hec, reg2hw.prio53.q, 1, 'h3, 0))
- `ASSERT(prio53_rd_A, rd_P(10'hec, reg2hw.prio53.q, 'hffffffff, 0))
-
- // assertions for register: prio54
- `ASSERT(prio54_wr_A, wr_P(10'hf0, reg2hw.prio54.q, 1, 'h3, 0))
- `ASSERT(prio54_rd_A, rd_P(10'hf0, reg2hw.prio54.q, 'hffffffff, 0))
-
- // assertions for register: prio55
- `ASSERT(prio55_wr_A, wr_P(10'hf4, reg2hw.prio55.q, 1, 'h3, 0))
- `ASSERT(prio55_rd_A, rd_P(10'hf4, reg2hw.prio55.q, 'hffffffff, 0))
-
- // assertions for register: prio56
- `ASSERT(prio56_wr_A, wr_P(10'hf8, reg2hw.prio56.q, 1, 'h3, 0))
- `ASSERT(prio56_rd_A, rd_P(10'hf8, reg2hw.prio56.q, 'hffffffff, 0))
-
- // assertions for register: prio57
- `ASSERT(prio57_wr_A, wr_P(10'hfc, reg2hw.prio57.q, 1, 'h3, 0))
- `ASSERT(prio57_rd_A, rd_P(10'hfc, reg2hw.prio57.q, 'hffffffff, 0))
-
- // assertions for register: prio58
- `ASSERT(prio58_wr_A, wr_P(10'h100, reg2hw.prio58.q, 1, 'h3, 0))
- `ASSERT(prio58_rd_A, rd_P(10'h100, reg2hw.prio58.q, 'hffffffff, 0))
-
- // assertions for register: prio59
- `ASSERT(prio59_wr_A, wr_P(10'h104, reg2hw.prio59.q, 1, 'h3, 0))
- `ASSERT(prio59_rd_A, rd_P(10'h104, reg2hw.prio59.q, 'hffffffff, 0))
-
- // assertions for register: prio60
- `ASSERT(prio60_wr_A, wr_P(10'h108, reg2hw.prio60.q, 1, 'h3, 0))
- `ASSERT(prio60_rd_A, rd_P(10'h108, reg2hw.prio60.q, 'hffffffff, 0))
-
- // assertions for register: prio61
- `ASSERT(prio61_wr_A, wr_P(10'h10c, reg2hw.prio61.q, 1, 'h3, 0))
- `ASSERT(prio61_rd_A, rd_P(10'h10c, reg2hw.prio61.q, 'hffffffff, 0))
-
- // assertions for register: prio62
- `ASSERT(prio62_wr_A, wr_P(10'h110, reg2hw.prio62.q, 1, 'h3, 0))
- `ASSERT(prio62_rd_A, rd_P(10'h110, reg2hw.prio62.q, 'hffffffff, 0))
-
- // assertions for register: prio63
- `ASSERT(prio63_wr_A, wr_P(10'h114, reg2hw.prio63.q, 1, 'h3, 0))
- `ASSERT(prio63_rd_A, rd_P(10'h114, reg2hw.prio63.q, 'hffffffff, 0))
-
- // assertions for register: prio64
- `ASSERT(prio64_wr_A, wr_P(10'h118, reg2hw.prio64.q, 1, 'h3, 0))
- `ASSERT(prio64_rd_A, rd_P(10'h118, reg2hw.prio64.q, 'hffffffff, 0))
-
- // assertions for register: prio65
- `ASSERT(prio65_wr_A, wr_P(10'h11c, reg2hw.prio65.q, 1, 'h3, 0))
- `ASSERT(prio65_rd_A, rd_P(10'h11c, reg2hw.prio65.q, 'hffffffff, 0))
-
- // assertions for register: prio66
- `ASSERT(prio66_wr_A, wr_P(10'h120, reg2hw.prio66.q, 1, 'h3, 0))
- `ASSERT(prio66_rd_A, rd_P(10'h120, reg2hw.prio66.q, 'hffffffff, 0))
-
- // assertions for register: prio67
- `ASSERT(prio67_wr_A, wr_P(10'h124, reg2hw.prio67.q, 1, 'h3, 0))
- `ASSERT(prio67_rd_A, rd_P(10'h124, reg2hw.prio67.q, 'hffffffff, 0))
-
- // assertions for register: prio68
- `ASSERT(prio68_wr_A, wr_P(10'h128, reg2hw.prio68.q, 1, 'h3, 0))
- `ASSERT(prio68_rd_A, rd_P(10'h128, reg2hw.prio68.q, 'hffffffff, 0))
-
- // assertions for register: prio69
- `ASSERT(prio69_wr_A, wr_P(10'h12c, reg2hw.prio69.q, 1, 'h3, 0))
- `ASSERT(prio69_rd_A, rd_P(10'h12c, reg2hw.prio69.q, 'hffffffff, 0))
-
- // assertions for register: prio70
- `ASSERT(prio70_wr_A, wr_P(10'h130, reg2hw.prio70.q, 1, 'h3, 0))
- `ASSERT(prio70_rd_A, rd_P(10'h130, reg2hw.prio70.q, 'hffffffff, 0))
-
- // assertions for register: prio71
- `ASSERT(prio71_wr_A, wr_P(10'h134, reg2hw.prio71.q, 1, 'h3, 0))
- `ASSERT(prio71_rd_A, rd_P(10'h134, reg2hw.prio71.q, 'hffffffff, 0))
-
- // assertions for register: prio72
- `ASSERT(prio72_wr_A, wr_P(10'h138, reg2hw.prio72.q, 1, 'h3, 0))
- `ASSERT(prio72_rd_A, rd_P(10'h138, reg2hw.prio72.q, 'hffffffff, 0))
-
- // assertions for register: prio73
- `ASSERT(prio73_wr_A, wr_P(10'h13c, reg2hw.prio73.q, 1, 'h3, 0))
- `ASSERT(prio73_rd_A, rd_P(10'h13c, reg2hw.prio73.q, 'hffffffff, 0))
-
- // assertions for register: prio74
- `ASSERT(prio74_wr_A, wr_P(10'h140, reg2hw.prio74.q, 1, 'h3, 0))
- `ASSERT(prio74_rd_A, rd_P(10'h140, reg2hw.prio74.q, 'hffffffff, 0))
-
- // assertions for register: prio75
- `ASSERT(prio75_wr_A, wr_P(10'h144, reg2hw.prio75.q, 1, 'h3, 0))
- `ASSERT(prio75_rd_A, rd_P(10'h144, reg2hw.prio75.q, 'hffffffff, 0))
-
- // assertions for register: prio76
- `ASSERT(prio76_wr_A, wr_P(10'h148, reg2hw.prio76.q, 1, 'h3, 0))
- `ASSERT(prio76_rd_A, rd_P(10'h148, reg2hw.prio76.q, 'hffffffff, 0))
-
- // assertions for register: prio77
- `ASSERT(prio77_wr_A, wr_P(10'h14c, reg2hw.prio77.q, 1, 'h3, 0))
- `ASSERT(prio77_rd_A, rd_P(10'h14c, reg2hw.prio77.q, 'hffffffff, 0))
-
- // assertions for register: prio78
- `ASSERT(prio78_wr_A, wr_P(10'h150, reg2hw.prio78.q, 1, 'h3, 0))
- `ASSERT(prio78_rd_A, rd_P(10'h150, reg2hw.prio78.q, 'hffffffff, 0))
-
- // assertions for register: prio79
- `ASSERT(prio79_wr_A, wr_P(10'h154, reg2hw.prio79.q, 1, 'h3, 0))
- `ASSERT(prio79_rd_A, rd_P(10'h154, reg2hw.prio79.q, 'hffffffff, 0))
-
- // assertions for register: prio80
- `ASSERT(prio80_wr_A, wr_P(10'h158, reg2hw.prio80.q, 1, 'h3, 0))
- `ASSERT(prio80_rd_A, rd_P(10'h158, reg2hw.prio80.q, 'hffffffff, 0))
-
- // assertions for register: prio81
- `ASSERT(prio81_wr_A, wr_P(10'h15c, reg2hw.prio81.q, 1, 'h3, 0))
- `ASSERT(prio81_rd_A, rd_P(10'h15c, reg2hw.prio81.q, 'hffffffff, 0))
-
- // assertions for register: prio82
- `ASSERT(prio82_wr_A, wr_P(10'h160, reg2hw.prio82.q, 1, 'h3, 0))
- `ASSERT(prio82_rd_A, rd_P(10'h160, reg2hw.prio82.q, 'hffffffff, 0))
-
- // define local fpv variable for multi-reg
- logic [82:0] ie0_q_fpv;
- for (genvar s = 0; s < 83; s++) begin : gen_ie0_q
- assign ie0_q_fpv[((s+1)*1-1):s*1] = reg2hw.ie0[s].q;
- end
-
- // assertions for register: ie00
- `ASSERT(ie00_wr_A, wr_P(10'h200, ie0_q_fpv[31:0], 1, 'hffffffff, 0))
- `ASSERT(ie00_rd_A, rd_P(10'h200, ie0_q_fpv[31:0], 'hffffffff, 0))
- // assertions for register: ie01
- `ASSERT(ie01_wr_A, wr_P(10'h204, ie0_q_fpv[63:32], 1, 'hffffffff, 0))
- `ASSERT(ie01_rd_A, rd_P(10'h204, ie0_q_fpv[63:32], 'hffffffff, 0))
- // assertions for register: ie02
- `ASSERT(ie02_wr_A, wr_P(10'h208, ie0_q_fpv[82:64], 1, 'h7ffff, 0))
- `ASSERT(ie02_rd_A, rd_P(10'h208, ie0_q_fpv[82:64], 'h7ffff, 0))
-
- // assertions for register: threshold0
- `ASSERT(threshold0_wr_A, wr_P(10'h20c, reg2hw.threshold0.q, 1, 'h3, 0))
- `ASSERT(threshold0_rd_A, rd_P(10'h20c, reg2hw.threshold0.q, 'hffffffff, 0))
-
- // assertions for register: cc0
- `ASSERT(cc0_wr_A, wr_ext_P(10'h210, reg2hw.cc0.q, 1, 'h7f, 0))
- `ASSERT(cc0_rd_A, rd_ext_P(10'h210, hw2reg.cc0.d, 'hffffffff, 0))
-
- // assertions for register: msip0
- `ASSERT(msip0_wr_A, wr_P(10'h214, reg2hw.msip0.q, 1, 'h1, 0))
- `ASSERT(msip0_rd_A, rd_P(10'h214, reg2hw.msip0.q, 'hffffffff, 0))
-
-
-endmodule
diff --git a/hw/top_earlgrey/ip/rv_plic/fpv/autogen/rv_plic_fpv.core b/hw/top_earlgrey/ip/rv_plic/fpv/autogen/rv_plic_fpv.core
index fd5c59f..507e02d 100644
--- a/hw/top_earlgrey/ip/rv_plic/fpv/autogen/rv_plic_fpv.core
+++ b/hw/top_earlgrey/ip/rv_plic/fpv/autogen/rv_plic_fpv.core
@@ -10,12 +10,19 @@
depend:
- lowrisc:fpv:rv_plic_component_fpv
- lowrisc:top_earlgrey:rv_plic
+ - lowrisc:fpv:csr_assert_gen
files:
- - rv_plic_csr_assert_fpv.sv
- rv_plic_bind_fpv.sv
- rv_plic_fpv.sv
file_type: systemVerilogSource
+generate:
+ csr_assert_gen:
+ generator: csr_assert_gen
+ parameters:
+ spec: ../../data/autogen/rv_plic.hjson
+ depend: lowrisc:top_earlgrey:rv_plic
+
targets:
default: &default_target
# note, this setting is just used
@@ -23,6 +30,8 @@
default_tool: icarus
filesets:
- files_formal
+ generate:
+ - csr_assert_gen
toplevel: rv_plic_fpv
formal:
diff --git a/util/fpvgen/fusesoc.core.tpl b/util/fpvgen/fusesoc.core.tpl
index 5778dea..5f64dda 100644
--- a/util/fpvgen/fusesoc.core.tpl
+++ b/util/fpvgen/fusesoc.core.tpl
@@ -9,17 +9,26 @@
depend:
% for dep in dut.deps:
- ${dep}
+ % if dut.is_cip:
+ - lowrisc:fpv:csr_assert_gen
+ % endif
% endfor
# TODO: add more dependencies here if needed
files:
- vip/${dut.name}_assert_fpv.sv
- tb/${dut.name}_bind_fpv.sv
- tb/${dut.name}_fpv.sv
-% if dut.is_cip:
- - vip/${dut.name}_csr_assert_fpv.sv
-% endif
file_type: systemVerilogSource
+% if dut.is_cip:
+generate:
+ csr_assert_gen:
+ generator: csr_assert_gen
+ parameters:
+ spec: ../data/${dut_name}.hjson
+ depend: lowrisc:ip:${dut_name}
+% endif
+
targets:
default: &default_target
# note, this setting is just used
@@ -27,6 +36,10 @@
default_tool: icarus
filesets:
- files_formal
+% if dut.is_cip:
+ generate:
+ - csr_assert_gen
+% endif
toplevel: ${dut.name}_fpv
formal:
diff --git a/util/topgen.py b/util/topgen.py
index e2651c2..01d2ec8 100755
--- a/util/topgen.py
+++ b/util/topgen.py
@@ -17,7 +17,7 @@
from mako.template import Template
import tlgen
-from reggen import gen_dv, gen_fpv, gen_rtl, validate
+from reggen import gen_dv, gen_rtl, validate
from topgen import (amend_clocks, get_hjsonobj_xbars, merge_top, search_ips,
validate_top)
@@ -260,7 +260,6 @@
object_pairs_hook=OrderedDict)
validate.validate(hjson_obj)
gen_rtl.gen_rtl(hjson_obj, str(rtl_path))
- gen_fpv.gen_fpv(hjson_obj, str(fpv_path))
# Generate RV_PLIC Top Module
with rtl_tpl_path.open(mode='r', encoding='UTF-8') as fin:
