[dv/full_chip] Fix pwrmgr_rstmgr SVA This SVA has two problems: - The main_rst_req_i (connected to !rst_main_n) should be ignored while in deep sleep low power. - The ndm_sys_req input is not seen by pwrmgr, so this assertion needs to be bound to top_earlgrey at chip level. The latter problem needs manipulation of the binds for pwrmgr and the creation of a new top_earlgrey bind for this specific SVA. Signed-off-by: Guillermo Maturana <maturana@google.com>
diff --git a/hw/ip/pwrmgr/dv/pwrmgr_sim_cfg.hjson b/hw/ip/pwrmgr/dv/pwrmgr_sim_cfg.hjson index 770b13e..250e762 100644 --- a/hw/ip/pwrmgr/dv/pwrmgr_sim_cfg.hjson +++ b/hw/ip/pwrmgr/dv/pwrmgr_sim_cfg.hjson
@@ -43,7 +43,8 @@ ] // Add additional tops for simulation. - sim_tops: ["pwrmgr_bind"] + sim_tops: ["pwrmgr_bind", + "pwrmgr_rstmgr_bind"] // Default iterations for all tests - each test entry can override this. reseed: 50
diff --git a/hw/ip/pwrmgr/dv/sva/pwrmgr_bind.sv b/hw/ip/pwrmgr/dv/sva/pwrmgr_bind.sv index 3d63d34..d6cefd8 100644 --- a/hw/ip/pwrmgr/dv/sva/pwrmgr_bind.sv +++ b/hw/ip/pwrmgr/dv/sva/pwrmgr_bind.sv
@@ -53,26 +53,4 @@ .usb_status(pwr_clk_i.usb_status) ); - bind pwrmgr pwrmgr_rstmgr_sva_if pwrmgr_rstmgr_sva_if ( - .clk_i, - .rst_ni, - .clk_slow_i, - .rst_slow_ni, - // Input resets. - .rstreqs_i(rstreqs_i), - .reset_en(reg2hw.reset_en), - .sw_rst_req_i(prim_mubi_pkg::mubi4_test_true_strict(sw_rst_req_i)), - .main_rst_req_i(rst_main_ni), - .esc_rst_req_i(esc_rst_req), - // The outputs from pwrmgr. - .rst_lc_req(pwr_rst_o.rst_lc_req), - .rst_sys_req(pwr_rst_o.rst_sys_req), - .rstreqs(pwr_rst_o.rstreqs), - .ndm_sys_req(1'b0), - .reset_cause(pwr_rst_o.reset_cause), - // The inputs from rstmgr. - .rst_lc_src_n(pwr_rst_i.rst_lc_src_n), - .rst_sys_src_n(pwr_rst_i.rst_sys_src_n) - ); - endmodule
diff --git a/hw/ip/pwrmgr/dv/sva/pwrmgr_rstmgr_bind.sv b/hw/ip/pwrmgr/dv/sva/pwrmgr_rstmgr_bind.sv new file mode 100644 index 0000000..a818243 --- /dev/null +++ b/hw/ip/pwrmgr/dv/sva/pwrmgr_rstmgr_bind.sv
@@ -0,0 +1,34 @@ +// Copyright lowRISC contributors. +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 + +// This is split off from pwrmgr_bind so that we can instantiate that in chip top, but +// specialize the bind of pwrmgr_rstmgr_sva_if for top_earlgrey, which is needed in order +// to hook up ndm_sys_req because pwrmgr doesn't see it. +module pwrmgr_rstmgr_bind; + + bind pwrmgr pwrmgr_rstmgr_sva_if pwrmgr_rstmgr_sva_if ( + .clk_i, + .rst_ni, + .clk_slow_i, + .rst_slow_ni, + // Input resets. + .rstreqs_i(rstreqs_i), + .reset_en(reg2hw.reset_en), + .sw_rst_req_i(prim_mubi_pkg::mubi4_test_true_strict(sw_rst_req_i)), + .main_rst_req_i(!rst_main_ni), + .esc_rst_req_i(esc_rst_req), + // The outputs from pwrmgr. + .rst_lc_req(pwr_rst_o.rst_lc_req), + .rst_sys_req(pwr_rst_o.rst_sys_req), + .rstreqs(pwr_rst_o.rstreqs), + .main_pd_n(pwr_ast_o.main_pd_n), + .reset_cause(pwr_rst_o.reset_cause), + // This goes directly to rstmgr and can trigger rst_sys_src_n. + .ndm_sys_req(1'b0), + // The inputs from rstmgr. + .rst_lc_src_n(pwr_rst_i.rst_lc_src_n), + .rst_sys_src_n(pwr_rst_i.rst_sys_src_n) + ); + +endmodule
diff --git a/hw/ip/pwrmgr/dv/sva/pwrmgr_rstmgr_sva_if.sv b/hw/ip/pwrmgr/dv/sva/pwrmgr_rstmgr_sva_if.sv index d5121f7..0ec5a02 100644 --- a/hw/ip/pwrmgr/dv/sva/pwrmgr_rstmgr_sva_if.sv +++ b/hw/ip/pwrmgr/dv/sva/pwrmgr_rstmgr_sva_if.sv
@@ -22,6 +22,7 @@ input logic [PowerDomains-1:0] rst_lc_req, input logic [PowerDomains-1:0] rst_sys_req, input logic [HwResetWidth-1:0] rstreqs, + input logic main_pd_n, input logic ndm_sys_req, input reset_cause_e reset_cause, // The inputs from rstmgr. @@ -95,9 +96,22 @@ ) |-> `RST_CYCLES !rstreqs[rst], clk_slow_i, reset_or_disable || !check_rstreqs_en) end + // This is used to ignore main_rst_req_i (wired to rst_main_n) if it happens during low power, + // since as part of deep sleep rst_main_n will trigger and not because of a power glitch. + logic rst_main_n_ignored_for_main_pwr_rst; + always_ff @(posedge clk_slow_i or negedge rst_slow_ni) begin + if (!rst_slow_ni) begin + rst_main_n_ignored_for_main_pwr_rst <= 0; + end else if (!main_pd_n && reset_cause == LowPwrEntry) begin + rst_main_n_ignored_for_main_pwr_rst <= 1; + end else if (reset_cause != LowPwrEntry) begin + rst_main_n_ignored_for_main_pwr_rst <= 0; + end + end + `ASSERT(MainPwrRstOn_A, $rose( - main_rst_req_i + main_rst_req_i && !rst_main_n_ignored_for_main_pwr_rst ) |-> `RST_CYCLES rstreqs[ResetMainPwrIdx], clk_slow_i, reset_or_disable || !check_rstreqs_en) `ASSERT(MainPwrRstOff_A,
diff --git a/hw/ip/pwrmgr/dv/sva/pwrmgr_sva.core b/hw/ip/pwrmgr/dv/sva/pwrmgr_sva.core index 34f9d38..ed1da2e 100644 --- a/hw/ip/pwrmgr/dv/sva/pwrmgr_sva.core +++ b/hw/ip/pwrmgr/dv/sva/pwrmgr_sva.core
@@ -14,6 +14,7 @@ - lowrisc:dv:pwrmgr_rstmgr_sva_if files: - pwrmgr_bind.sv + - pwrmgr_rstmgr_bind.sv - pwrmgr_ast_sva_if.sv - pwrmgr_clock_enables_sva_if.sv file_type: systemVerilogSource
diff --git a/hw/ip/rstmgr/dv/sva/rstmgr_bind.sv b/hw/ip/rstmgr/dv/sva/rstmgr_bind.sv index 8c0af9f..d2d8f25 100644 --- a/hw/ip/rstmgr/dv/sva/rstmgr_bind.sv +++ b/hw/ip/rstmgr/dv/sva/rstmgr_bind.sv
@@ -28,6 +28,7 @@ // These are actually used for checks. .rst_lc_req(pwr_i.rst_lc_req), .rst_sys_req(pwr_i.rst_sys_req), + .main_pd_n('1), .ndm_sys_req(ndmreset_req_i), .reset_cause(pwr_i.reset_cause), // The inputs from rstmgr.
diff --git a/hw/top_earlgrey/dv/chip_sim.core b/hw/top_earlgrey/dv/chip_sim.core index b359896..dff5c3d 100644 --- a/hw/top_earlgrey/dv/chip_sim.core +++ b/hw/top_earlgrey/dv/chip_sim.core
@@ -18,6 +18,7 @@ - lowrisc:dv:clkmgr_sva - lowrisc:dv:pwrmgr_sva - lowrisc:dv:rstmgr_sva + - lowrisc:dv:top_earlgrey_sva - lowrisc:dv:xbar_main_bind - lowrisc:dv:xbar_peri_bind - lowrisc:dv:xbar_test
diff --git a/hw/top_earlgrey/dv/chip_sim_cfg.hjson b/hw/top_earlgrey/dv/chip_sim_cfg.hjson index 93e10d8..eb115a9 100644 --- a/hw/top_earlgrey/dv/chip_sim_cfg.hjson +++ b/hw/top_earlgrey/dv/chip_sim_cfg.hjson
@@ -27,6 +27,7 @@ sim_tops: ["clkmgr_bind", "pwrmgr_bind", "rstmgr_bind", + "top_earlgrey_bind", "xbar_main_bind", "xbar_peri_bind"]
diff --git a/hw/top_earlgrey/dv/sva/top_earlgrey_bind.sv b/hw/top_earlgrey/dv/sva/top_earlgrey_bind.sv new file mode 100644 index 0000000..bb1121e --- /dev/null +++ b/hw/top_earlgrey/dv/sva/top_earlgrey_bind.sv
@@ -0,0 +1,33 @@ +// Copyright lowRISC contributors. +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 + +module top_earlgrey_bind; + + // This is bound directly to top_earlgrey since neither pwrmgr nor rstmgr see all necessary + // signals. + bind top_earlgrey pwrmgr_rstmgr_sva_if pwrmgr_rstmgr_sva_if ( + .clk_i(u_pwrmgr_aon.clk_i), + .rst_ni(u_pwrmgr_aon.rst_ni), + .clk_slow_i(u_pwrmgr_aon.clk_slow_i), + .rst_slow_ni(u_pwrmgr_aon.rst_slow_ni), + // Input resets. + .rstreqs_i(u_pwrmgr_aon.rstreqs_i), + .reset_en(u_pwrmgr_aon.reg2hw.reset_en), + .sw_rst_req_i(prim_mubi_pkg::mubi4_test_true_strict(u_pwrmgr_aon.sw_rst_req_i)), + .main_rst_req_i(!u_pwrmgr_aon.rst_main_ni), + .esc_rst_req_i(u_pwrmgr_aon.esc_rst_req), + // The outputs from pwrmgr. + .rst_lc_req(u_pwrmgr_aon.pwr_rst_o.rst_lc_req), + .rst_sys_req(u_pwrmgr_aon.pwr_rst_o.rst_sys_req), + .rstreqs(u_pwrmgr_aon.pwr_rst_o.rstreqs), + .main_pd_n(u_pwrmgr_aon.pwr_ast_o.main_pd_n), + .reset_cause(u_pwrmgr_aon.pwr_rst_o.reset_cause), + // This goes directly to rstmgr and can trigger rst_sys_src_n. + .ndm_sys_req(u_rstmgr_aon.ndmreset_req_i), + // The inputs from rstmgr. + .rst_lc_src_n(u_pwrmgr_aon.pwr_rst_i.rst_lc_src_n), + .rst_sys_src_n(u_pwrmgr_aon.pwr_rst_i.rst_sys_src_n) + ); + +endmodule
diff --git a/hw/top_earlgrey/dv/sva/top_earlgrey_sva.core b/hw/top_earlgrey/dv/sva/top_earlgrey_sva.core new file mode 100644 index 0000000..c242b37 --- /dev/null +++ b/hw/top_earlgrey/dv/sva/top_earlgrey_sva.core
@@ -0,0 +1,24 @@ +CAPI=2: +# Copyright lowRISC contributors. +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 +name: "lowrisc:dv:top_earlgrey_sva:0.1" +description: "TOP_EARLGREY assertion modules and bind file." +filesets: + files_dv: + depend: + - lowrisc:systems:top_earlgrey + - lowrisc:dv:pwrmgr_rstmgr_sva_if + files: + - top_earlgrey_bind.sv + file_type: systemVerilogSource + +targets: + default: &default_target + filesets: + - files_dv + formal: + <<: *default_target + filesets: + - files_dv + toplevel: top_earlgrey_bind