[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