[fpv/pwrmgr] Add pwrmgr and top_earlgrey to FPV
Add pwrmgr_bind.sv file
Add pwrmgr to FPV run
Add formal target in top_eargrey core
Delete FPV folder in pwrmgr
Signed-off-by: Cindy Chen <chencindy@google.com>
diff --git a/hw/formal/fpv_all b/hw/formal/fpv_all
index d4593bf..8585837 100755
--- a/hw/formal/fpv_all
+++ b/hw/formal/fpv_all
@@ -26,6 +26,7 @@
"uart"
"hmac"
"flash_ctrl"
+ "pwrmgr"
"usbuart"
"usbdev"
"usb_fs_nb_pe"
diff --git a/hw/ip/pwrmgr/dv/tb/pwrmgr_bind.sv b/hw/ip/pwrmgr/dv/tb/pwrmgr_bind.sv
new file mode 100644
index 0000000..fe57be2
--- /dev/null
+++ b/hw/ip/pwrmgr/dv/tb/pwrmgr_bind.sv
@@ -0,0 +1,16 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+module pwrmgr_bind;
+
+ bind pwrmgr tlul_assert #(
+ .EndpointType("Device")
+ ) tlul_assert_device (
+ .clk_i,
+ .rst_ni,
+ .h2d (tl_i),
+ .d2h (tl_o)
+ );
+
+endmodule
diff --git a/hw/ip/pwrmgr/fpv/vip/pwrmgr_csr_assert_fpv.sv b/hw/ip/pwrmgr/fpv/vip/pwrmgr_csr_assert_fpv.sv
deleted file mode 100644
index d20d505..0000000
--- a/hw/ip/pwrmgr/fpv/vip/pwrmgr_csr_assert_fpv.sv
+++ /dev/null
@@ -1,134 +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
-
-
-`include "prim_assert.sv"
-
-// Block: pwrmgr
-module pwrmgr_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;
-
- // 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
- property wr_P(int width, bit [5: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 [5: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 [5: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 [5: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
-
- // read/write assertions for register: intr_state
- `ASSERT(intr_state_wr_A, wr_P(0, 6'h0, i_pwrmgr.reg2hw.intr_state.q, 0))
- `ASSERT(intr_state_rd_A, rd_P(0, 6'h0, i_pwrmgr.hw2reg.intr_state.d))
-
- // read/write assertions for register: intr_enable
- `ASSERT(intr_enable_wr_A, wr_P(0, 6'h4, i_pwrmgr.reg2hw.intr_enable.q, 0))
- `ASSERT(intr_enable_rd_A, rd_P(0, 6'h4, i_pwrmgr.reg2hw.intr_enable.q))
-
- // read/write assertions for register: intr_test
- `ASSERT(intr_test_wr_A, wr_ext_P(0, 6'h8, i_pwrmgr.reg2hw.intr_test.q, 0))
-
- // read/write assertions for register: ctrl_cfg_regwen
- `ASSERT(ctrl_cfg_regwen_rd_A, rd_ext_P(0, 6'hc, i_pwrmgr.hw2reg.ctrl_cfg_regwen.d))
-
- // read/write assertions for register: control
- `ASSERT(control_wr_A, wr_P(6, 6'h10, i_pwrmgr.reg2hw.control.q, i_pwrmgr.i_reg_top.ctrl_cfg_regwen_qs))
- `ASSERT(control_stable_A, wr_regen_stable_P(i_pwrmgr.i_reg_top.ctrl_cfg_regwen_qs, i_pwrmgr.reg2hw.control.q))
- `ASSERT(control_rd_A, rd_P(6, 6'h10, i_pwrmgr.hw2reg.control.d))
-
- // read/write assertions for register: cfg_cdc_sync
- `ASSERT(cfg_cdc_sync_wr_A, wr_P(0, 6'h14, i_pwrmgr.reg2hw.cfg_cdc_sync.q, 0))
- `ASSERT(cfg_cdc_sync_rd_A, rd_P(0, 6'h14, i_pwrmgr.hw2reg.cfg_cdc_sync.d))
-
- // read/write assertions for register: wakeup_en_regwen
- `ASSERT(wakeup_en_regwen_wr_A, wr_P(0, 6'h18, i_pwrmgr.i_reg_top.wakeup_en_regwen_we, 0))
- `ASSERT(wakeup_en_regwen_rd_A, rd_P(0, 6'h18, i_pwrmgr.i_reg_top.wakeup_en_regwen_qs))
-
- // read/write assertions for register: wakeup_en
- `ASSERT(wakeup_en_wr_A, wr_P(15, 6'h1c, i_pwrmgr.reg2hw.wakeup_en.q, i_pwrmgr.i_reg_top.wakeup_en_regwen_qs))
- `ASSERT(wakeup_en_stable_A, wr_regen_stable_P(i_pwrmgr.i_reg_top.wakeup_en_regwen_qs, i_pwrmgr.reg2hw.wakeup_en.q))
- `ASSERT(wakeup_en_rd_A, rd_P(15, 6'h1c, i_pwrmgr.reg2hw.wakeup_en.q))
-
- // read/write assertions for register: wake_status
- `ASSERT(wake_status_rd_A, rd_P(15, 6'h20, i_pwrmgr.i_reg_top.wake_status_qs))
-
- // read/write assertions for register: reset_en_regwen
- `ASSERT(reset_en_regwen_wr_A, wr_P(0, 6'h24, i_pwrmgr.i_reg_top.reset_en_regwen_we, 0))
- `ASSERT(reset_en_regwen_rd_A, rd_P(0, 6'h24, i_pwrmgr.i_reg_top.reset_en_regwen_qs))
-
- // read/write assertions for register: reset_en
- `ASSERT(reset_en_wr_A, wr_P(1, 6'h28, i_pwrmgr.reg2hw.reset_en.q, i_pwrmgr.i_reg_top.reset_en_regwen_qs))
- `ASSERT(reset_en_stable_A, wr_regen_stable_P(i_pwrmgr.i_reg_top.reset_en_regwen_qs, i_pwrmgr.reg2hw.reset_en.q))
- `ASSERT(reset_en_rd_A, rd_P(1, 6'h28, i_pwrmgr.reg2hw.reset_en.q))
-
- // read/write assertions for register: reset_status
- `ASSERT(reset_status_rd_A, rd_P(1, 6'h2c, i_pwrmgr.i_reg_top.reset_status_qs))
-
- // read/write assertions for register: wake_info_capture_dis
- `ASSERT(wake_info_capture_dis_wr_A, wr_P(0, 6'h30, i_pwrmgr.reg2hw.wake_info_capture_dis.q, 0))
- `ASSERT(wake_info_capture_dis_rd_A, rd_P(0, 6'h30, i_pwrmgr.reg2hw.wake_info_capture_dis.q))
-
- // read/write assertions for register: wake_info
- `ASSERT(wake_info_wr_A, wr_ext_P(17, 6'h34, i_pwrmgr.reg2hw.wake_info.q, 0))
- `ASSERT(wake_info_rd_A, rd_ext_P(17, 6'h34, i_pwrmgr.hw2reg.wake_info.d))
-
-endmodule
diff --git a/hw/top_earlgrey/top_earlgrey.core b/hw/top_earlgrey/top_earlgrey.core
index 1f4f15b..e018fa9 100644
--- a/hw/top_earlgrey/top_earlgrey.core
+++ b/hw/top_earlgrey/top_earlgrey.core
@@ -109,3 +109,7 @@
parameters:
- SYNTHESIS=true
toplevel: top_earlgrey
+
+ formal:
+ <<: *default_target
+ toplevel: top_earlgrey
