From ce432600ab841f393403de063ba4d7ed9e75f52e Mon Sep 17 00:00:00 2001 From: maksyuki Date: Tue, 4 Aug 2026 21:35:02 +0800 Subject: [PATCH] feat: update sysctrl formal properties to include user_core_count and user_reset_mask --- rtl/mini/formal/sysctrl_formal.sv | 8 ++++++-- rtl/mini/formal/sysctrl_formal_props.sv | 15 ++++++++++----- tests/test_script_tools.py | 11 +++++++++++ 3 files changed, 27 insertions(+), 7 deletions(-) diff --git a/rtl/mini/formal/sysctrl_formal.sv b/rtl/mini/formal/sysctrl_formal.sv index 3b020159..fe677334 100644 --- a/rtl/mini/formal/sysctrl_formal.sv +++ b/rtl/mini/formal/sysctrl_formal.sv @@ -12,7 +12,9 @@ module sysctrl_formal_design ( output logic rib_ready, output logic [ 7:0] ip_sel, output logic [ 4:0] core_sel, - output logic [ 5:0] user_reset, + output logic [31:0] user_reset, + output logic [31:0] user_reset_mask, + output logic [ 5:0] user_core_count, output logic user_bus_enable, output logic user_config_error, output logic [ 2:0] pll_cfg, @@ -86,7 +88,9 @@ module sysctrl_formal_design ( assign rib_ready = rib.ready; assign ip_sel = sysctrl.ip_sel_o; assign core_sel = u_dut.s_sysctrl_coresel_q; - assign user_reset = u_dut.s_user_reset_q; + assign user_reset = {{(32 - `USER_CORE_COUNT) {1'b0}}, u_dut.s_user_reset_q}; + assign user_reset_mask = {{(32 - `USER_CORE_COUNT) {1'b0}}, {`USER_CORE_COUNT{1'b1}}}; + assign user_core_count = `USER_CORE_COUNT; assign user_bus_enable = u_dut.s_user_running_q; assign user_config_error = u_dut.s_user_config_error_q; assign pll_cfg = u_dut.s_pll_cfg_q; diff --git a/rtl/mini/formal/sysctrl_formal_props.sv b/rtl/mini/formal/sysctrl_formal_props.sv index 99e72d2f..6dd49163 100644 --- a/rtl/mini/formal/sysctrl_formal_props.sv +++ b/rtl/mini/formal/sysctrl_formal_props.sv @@ -19,7 +19,9 @@ module sysctrl_formal; wire rib_ready; wire [ 7:0] ip_sel; wire [ 4:0] core_sel; - wire [ 5:0] user_reset; + wire [31:0] user_reset; + wire [31:0] user_reset_mask; + wire [ 5:0] user_core_count; wire user_bus_enable; wire user_config_error; wire [ 2:0] pll_cfg; @@ -51,6 +53,8 @@ module sysctrl_formal; .ip_sel (ip_sel), .core_sel (core_sel), .user_reset (user_reset), + .user_reset_mask (user_reset_mask), + .user_core_count (user_core_count), .user_bus_enable (user_bus_enable), .user_config_error(user_config_error), .pll_cfg (pll_cfg), @@ -85,13 +89,14 @@ module sysctrl_formal; if (rst_n_i && f_past_valid) begin if ($past( rst_n_i && rib_valid && !rib_ready && rib_wstrb[0] && - rib_addr[7:0] == 8'h00 && rib_wdata[4:0] < 6 && user_reset == 6'h3f && !user_bus_enable + rib_addr[7:0] == 8'h00 && rib_wdata[4:0] < user_core_count && + user_reset == user_reset_mask && !user_bus_enable )) begin assert (core_sel == $past(rib_wdata[4:0])); end if ($past( rst_n_i && rib_valid && !rib_ready && rib_wstrb[0] && - rib_addr[7:0] == 8'h00 && rib_wdata[4:0] >= 6 + rib_addr[7:0] == 8'h00 && rib_wdata[4:0] >= user_core_count )) begin assert (core_sel == $past(core_sel)); assert (user_config_error); @@ -99,9 +104,9 @@ module sysctrl_formal; if ($past( rst_n_i && rib_valid && !rib_ready && rib_wstrb[0] && rib_addr[7:0] == SYSCTRL_USER_CORE_RESET_OFFSET && - rib_wdata[5:0] == 6'h3f + (rib_wdata & user_reset_mask) == user_reset_mask )) begin - assert (user_reset == 6'h3f); + assert (user_reset == user_reset_mask); assert (!user_bus_enable); end if ($past( diff --git a/tests/test_script_tools.py b/tests/test_script_tools.py index df6140d3..d171bb25 100644 --- a/tests/test_script_tools.py +++ b/tests/test_script_tools.py @@ -229,6 +229,17 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non assert ROOT / "rtl/mini/formal/gpio_user_formal.sv" in gpio_user.files +def test_sysctrl_formal_properties_use_exported_user_core_shape() -> None: + design = (ROOT / "rtl/mini/formal/sysctrl_formal.sv").read_text(encoding="utf-8") + properties = (ROOT / "rtl/mini/formal/sysctrl_formal_props.sv").read_text(encoding="utf-8") + + assert "user_reset_mask" in design + assert "user_core_count" in design + assert "`USER_CORE_COUNT" not in properties + assert "rib_wdata[4:0] < user_core_count" in properties + assert "user_reset == user_reset_mask" in properties + + def test_sby_config_uses_prove_and_cover_with_bitwuzla(tmp_path: Path) -> None: design = tmp_path / "design.v" properties = tmp_path / "properties.v"