feat: add formal for pll, sysctrl and rcu

Makefile

@@ -200,7 +200,7 @@ help:
 	  '  check-user-extensions      validate the canonical user-extension map' \
 	  '  check-clock-reset-domains  validate the root clock/reset and CDC inventory' \
 	  '  rtl-lint | check-rtl-lint  run/check strict Verilator RTL lint warnings' \
-	  '  formal | formal-bus | formal-nmi2apb prove Bus/NMI2APB protocol properties with SBY' \
+	  '  formal | formal-bus | formal-nmi2apb | formal-sysctrl | formal-pll-rcu | formal-gpio-mdd run SBY protocol proofs' \
 	  '  formal-doctor              check the SBY, Yosys, sv2v, and Bitwuzla formal toolchain' \
 	  '  tech-cell-test             test GF180/SKY130 technology IO and clock wrappers' \
 	  '  check-warnings | metrics   analyze flow logs and reports' \

config/dependencies.lock.json

@@ -78,7 +78,7 @@
   },
   "archives": {
     "fatfs": {
-      "url": "https://elm-chan.org/fsw/ff/arc/ff16.zip",
+      "url": "https://github.com/retroSoC/artifact/releases/download/fatfs-r0.16/fatfs-r0.16.zip",
       "sha256": "99f7dc1f7e095356e4a9e3dbe29959090d8b948afe2bbc5441e52fdf4b85449e",
       "destination": "app/fatfs/ff16/ff16.zip",
       "license": "LicenseRef-FatFs"

docs/engineering.md

@@ -108,8 +108,12 @@ marker is present. Icarus regressions use the assembly self-test as `retrosoc_as
 
 `make CONFIG=configs/ci/hazard3-rv32im-ihp130.mk formal` proves selected
 protocol invariants with SymbiYosys, Yosys, `sv2v`, and Bitwuzla. The current
-targets are `bus` and `nmi2apb`; each uses the SBY `prove` task for bounded
-model checking and k-induction, plus a `cover` task, at depth 20.
+targets are `bus`, `nmi2apb`, `sysctrl`, `pll_rcu`, and `gpio_mdd`; each uses
+the SBY `prove` task for bounded model checking and k-induction, plus a
+`cover` task, at depth 20. `sysctrl` checks register side effects, PLL request
+handling, and fault reporting. `pll_rcu` checks the clock-switch controller
+state machine. `gpio_mdd` checks MDD user-GPIO ownership, lock, handoff, and
+mux safety using the `IP_MDD` build definition.
 `FORMAL_DEPTH` and `FORMAL_TIMEOUT` set the proof bound and per-task
 wall-clock limit. Use `make CONFIG=<profile> formal-doctor` before a local
 proof to verify that the required tools are available.
@@ -129,6 +133,11 @@ repeat PDK-independent protocol proofs. The reusable regression workflow runs
 the target only when its `formal_checks` input is enabled and its locked
 toolset provides SBY and Bitwuzla.
 
+The `pll_rcu` proof uses one formal clock for its system and external-clock
+inputs to verify the controller protocol independently of analogue clock
+behavior. It is not asynchronous CDC/RDC signoff; implementation timing,
+clock-tree checks, and the technology PLL model remain separate signoff work.
+
 `make check-warnings` normalizes tool messages and compares them with
 `quality/warnings/<profile>/<tool>.json`. New signatures and increased counts fail; resolved warnings
 are reported but do not fail. To refresh one baseline after review:

rtl/mini/formal/generate_formal_filelist.py

@@ -18,9 +18,16 @@ from filelist import FileList, write_filelist  # noqa: E402
 
 COMMON_RTL = ROOT / "rtl/managed/clusterip/common/rtl"
 INTERCONNECT = ROOT / "rtl/ip/native/interconnect"
+PERIPHERAL = ROOT / "rtl/ip/native/peripheral"
 TOP = ROOT / "rtl/mini/top"
 
 
+def target_defines(target: str) -> list[str]:
+    if target == "gpio_mdd":
+        return ["+define+SV_ASSRT_DISABLE", "+define+IP_MDD"]
+    return ["+define+SV_ASSRT_DISABLE"]
+
+
 def source_files(target: str) -> list[Path]:
     common = [
         COMMON_RTL / "interface/nmi_if.sv",
@@ -42,12 +49,36 @@ def source_files(target: str) -> list[Path]:
             INTERCONNECT / "nmi2apb.sv",
             SCRIPT_DIR / "nmi2apb_formal.sv",
         ]
+    if target == "sysctrl":
+        return [
+            *common,
+            PERIPHERAL / "pll_ctrl_if.sv",
+            PERIPHERAL / "sysctrl.sv",
+            SCRIPT_DIR / "sysctrl_formal.sv",
+        ]
+    if target == "pll_rcu":
+        return [
+            *common,
+            COMMON_RTL / "cdc/cdc_sync.sv",
+            COMMON_RTL / "cdc/cdc_2phase.sv",
+            PERIPHERAL / "pll_ctrl_if.sv",
+            TOP / "rcu.sv",
+            SCRIPT_DIR / "pll_rcu_formal.sv",
+        ]
+    if target == "gpio_mdd":
+        return [
+            *common,
+            COMMON_RTL / "cdc/cdc_sync.sv",
+            COMMON_RTL / "utils/edge_det.sv",
+            PERIPHERAL / "gpio.sv",
+            SCRIPT_DIR / "gpio_mdd_formal.sv",
+        ]
     raise ValueError(f"unsupported formal target: {target}")
 
 
 def generate(target: str, output: Path, memory_map_dir: Path, soc_topology_dir: Path) -> bool:
     filelist = FileList(
-        defines=["+define+SV_ASSRT_DISABLE"],
+        defines=target_defines(target),
         incdirs=[
             memory_map_dir.resolve() / "rtl",
             soc_topology_dir.resolve() / "rtl",
@@ -56,6 +87,7 @@ def generate(target: str, output: Path, memory_map_dir: Path, soc_topology_dir:
             COMMON_RTL / "interface",
             COMMON_RTL / "utils",
             INTERCONNECT,
+            PERIPHERAL,
         ],
         files=source_files(target),
     ).deduplicate()
@@ -64,7 +96,11 @@ def generate(target: str, output: Path, memory_map_dir: Path, soc_topology_dir:
 
 def parse_args() -> argparse.Namespace:
     parser = argparse.ArgumentParser(description=__doc__)
-    parser.add_argument("--target", choices=("bus", "nmi2apb"), required=True)
+    parser.add_argument(
+        "--target",
+        choices=("bus", "nmi2apb", "sysctrl", "pll_rcu", "gpio_mdd"),
+        required=True,
+    )
     parser.add_argument("--output", type=Path, required=True)
     parser.add_argument("--memory-map-dir", type=Path, required=True)
     parser.add_argument("--soc-topology-dir", type=Path, required=True)

rtl/mini/formal/gpio_mdd_formal.sv

@@ -0,0 +1,91 @@
+// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
+// retroSoC is licensed under Mulan PSL v2.
+
+module gpio_mdd_formal_design (
+    input  logic        clk_i,
+    output logic        rst_n_i,
+    output logic        f_past_valid,
+    output logic        nmi_valid,
+    output logic [31:0] nmi_addr,
+    output logic [31:0] nmi_wdata,
+    output logic [ 3:0] nmi_wstrb,
+    output logic        nmi_ready,
+    output logic [31:0] gpio_di,
+    output logic [31:0] gpio_oe,
+    output logic [31:0] gpio_do,
+    output logic [31:0] user_di,
+    output logic [31:0] user_oe,
+    output logic [31:0] user_do,
+    output logic [31:0] user_sel,
+    output logic [31:0] user_lock,
+    output logic [31:0] user_handoff,
+    output logic [31:0] user_status,
+    output logic [31:0] native_oe,
+    output logic [31:0] native_do
+);
+
+  nmi_if nmi ();
+  gpio_if gpio ();
+  user_gpio_if user_gpio ();
+
+  (* anyseq *)logic        f_nmi_valid;
+  (* anyseq *)logic [31:0] f_nmi_addr;
+  (* anyseq *)logic [31:0] f_nmi_wdata;
+  (* anyseq *)logic [ 3:0] f_nmi_wstrb;
+  (* anyseq *)logic [31:0] f_gpio_di;
+  (* anyseq *)logic [31:0] f_alt0_do;
+  (* anyseq *)logic [31:0] f_alt0_oe;
+  (* anyseq *)logic [31:0] f_alt1_do;
+  (* anyseq *)logic [31:0] f_alt1_oe;
+  (* anyseq *)logic [31:0] f_user_do;
+  (* anyseq *)logic [31:0] f_user_oe;
+
+  assign nmi.valid      = f_nmi_valid;
+  assign nmi.addr       = f_nmi_addr;
+  assign nmi.wdata      = f_nmi_wdata;
+  assign nmi.wstrb      = f_nmi_wstrb;
+  assign gpio.di_i      = f_gpio_di;
+  assign gpio.alt0_do_i = f_alt0_do;
+  assign gpio.alt0_oe_i = f_alt0_oe;
+  assign gpio.alt1_do_i = f_alt1_do;
+  assign gpio.alt1_oe_i = f_alt1_oe;
+  assign user_gpio.do_o = f_user_do;
+  assign user_gpio.oe_o = f_user_oe;
+
+  assign nmi_valid      = nmi.valid;
+  assign nmi_addr       = nmi.addr;
+  assign nmi_wdata      = nmi.wdata;
+  assign nmi_wstrb      = nmi.wstrb;
+  assign nmi_ready      = nmi.ready;
+  assign gpio_di        = gpio.di_i;
+  assign gpio_oe        = gpio.oe_o;
+  assign gpio_do        = gpio.do_o;
+  assign user_di        = user_gpio.di_i;
+  assign user_oe        = user_gpio.oe_o;
+  assign user_do        = user_gpio.do_o;
+  assign user_sel       = u_dut.s_gpio_user_sel_q;
+  assign user_lock      = u_dut.s_gpio_user_lock_q;
+  assign user_handoff   = u_dut.s_gpio_user_handoff_q;
+  assign user_status    = u_dut.s_gpio_user_status;
+  assign native_oe      = u_dut.s_gpio_native_oe;
+  assign native_do      = u_dut.s_gpio_native_out;
+
+  nmi_gpio u_dut (
+      .clk_i    (clk_i),
+      .rst_n_i  (rst_n_i),
+      .nmi      (nmi),
+      .gpio     (gpio),
+      .user_gpio(user_gpio)
+  );
+
+  initial begin
+    rst_n_i      = 1'b0;
+    f_past_valid = 1'b0;
+  end
+
+  always_ff @(posedge clk_i) begin
+    rst_n_i      <= 1'b1;
+    f_past_valid <= 1'b1;
+  end
+
+endmodule

rtl/mini/formal/gpio_mdd_formal_props.v

@@ -0,0 +1,77 @@
+// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
+// retroSoC is licensed under Mulan PSL v2.
+
+module gpio_mdd_formal;
+
+  (* anyseq *) (* gclk *)reg         clk_i;
+  wire        rst_n_i;
+  wire        f_past_valid;
+  wire        nmi_valid;
+  wire [31:0] nmi_addr;
+  wire [31:0] nmi_wdata;
+  wire [ 3:0] nmi_wstrb;
+  wire        nmi_ready;
+  wire [31:0] gpio_di;
+  wire [31:0] gpio_oe;
+  wire [31:0] gpio_do;
+  wire [31:0] user_di;
+  wire [31:0] user_oe;
+  wire [31:0] user_do;
+  wire [31:0] user_sel;
+  wire [31:0] user_lock;
+  wire [31:0] user_handoff;
+  wire [31:0] user_status;
+  wire [31:0] native_oe;
+  wire [31:0] native_do;
+
+  gpio_mdd_formal_design u_design (
+      .clk_i       (clk_i),
+      .rst_n_i     (rst_n_i),
+      .f_past_valid(f_past_valid),
+      .nmi_valid   (nmi_valid),
+      .nmi_addr    (nmi_addr),
+      .nmi_wdata   (nmi_wdata),
+      .nmi_wstrb   (nmi_wstrb),
+      .nmi_ready   (nmi_ready),
+      .gpio_di     (gpio_di),
+      .gpio_oe     (gpio_oe),
+      .gpio_do     (gpio_do),
+      .user_di     (user_di),
+      .user_oe     (user_oe),
+      .user_do     (user_do),
+      .user_sel    (user_sel),
+      .user_lock   (user_lock),
+      .user_handoff(user_handoff),
+      .user_status (user_status),
+      .native_oe   (native_oe),
+      .native_do   (native_do)
+  );
+
+  always @(posedge clk_i) begin
+    if (f_past_valid && $past(rst_n_i && nmi_valid && !nmi_ready)) begin
+      assume (nmi_valid);
+      assume (nmi_addr == $past(nmi_addr));
+      assume (nmi_wdata == $past(nmi_wdata));
+      assume (nmi_wstrb == $past(nmi_wstrb));
+    end
+
+    if (rst_n_i) begin
+      assert (user_di == gpio_di);
+      assert(gpio_oe == ((~user_handoff & user_sel & user_oe) |
+                         (~user_handoff & ~user_sel & native_oe)));
+      assert (gpio_do == ((user_sel & user_do) | (~user_sel & native_do)));
+      assert (user_status == (user_sel & ~user_handoff));
+      if (f_past_valid) begin
+        assert (user_handoff == (user_sel ^ $past(user_sel)));
+        if ($past(user_lock)) begin
+          assert (user_lock);
+          assert ((user_sel & $past(user_lock)) == ($past(user_sel) & $past(user_lock)));
+        end
+      end
+      cover (|user_handoff);
+      cover (|user_lock && |user_sel);
+      cover (|user_status && |gpio_oe);
+    end
+  end
+
+endmodule

rtl/mini/formal/pll_rcu_formal.sv

@@ -0,0 +1,77 @@
+// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
+// retroSoC is licensed under Mulan PSL v2.
+
+module pll_rcu_formal_design (
+    input  logic       clk_i,
+    output logic       rst_n_i,
+    output logic       f_past_valid,
+    output logic       req_valid,
+    output logic [2:0] req_sel,
+    output logic       req_ready,
+    output logic       rsp_valid,
+    output logic       rsp_ready,
+    output logic       pll_lock,
+    output logic       pll_capable,
+    output logic [2:0] state,
+    output logic       pll_apply,
+    output logic       select_ext_clk,
+    output logic       active_valid,
+    output logic       safe_clk,
+    output logic       active_lock,
+    output logic [1:0] error
+);
+
+  pll_ctrl_if pll_ctrl ();
+
+  (* anyseq *)logic       f_req_valid;
+  (* anyseq *)logic [2:0] f_req_sel;
+  (* anyseq *)logic       f_rsp_ready;
+  (* anyseq *)logic       f_pll_lock;
+  (* anyseq *)logic       f_pll_capable;
+
+  assign pll_ctrl.req_valid_o = f_req_valid;
+  assign pll_ctrl.req_sel_o   = f_req_sel;
+  assign pll_ctrl.rsp_ready_o = f_rsp_ready;
+  assign req_valid            = pll_ctrl.req_valid_o;
+  assign req_sel              = pll_ctrl.req_sel_o;
+  assign req_ready            = pll_ctrl.req_ready_i;
+  assign rsp_valid            = pll_ctrl.rsp_valid_i;
+  assign rsp_ready            = pll_ctrl.rsp_ready_o;
+  assign pll_lock             = f_pll_lock;
+  assign pll_capable          = f_pll_capable;
+  assign state                = u_dut.s_state_q;
+  assign pll_apply            = u_dut.s_pll_apply_q;
+  assign select_ext_clk       = u_dut.s_select_ext_clk_q;
+  assign active_valid         = u_dut.s_active_valid_q;
+  assign safe_clk             = u_dut.s_safe_clk_q;
+  assign active_lock          = u_dut.s_lock_q;
+  assign error                = u_dut.s_error_q;
+
+  // Both controller domains share the formal clock. This proves the control
+  // FSM and the production cdc_2phase composition, not asynchronous CDC timing.
+  pll_rcu_controller #(
+      .LOCK_TIMEOUT(4)
+  ) u_dut (
+      .sys_clk_i       (clk_i),
+      .sys_rst_n_i     (rst_n_i),
+      .ext_clk_i       (clk_i),
+      .ext_rst_n_i     (rst_n_i),
+      .pll_lock_i      (f_pll_lock),
+      .pll_capable_i   (f_pll_capable),
+      .pll_sel_o       (),
+      .pll_apply_o     (),
+      .select_ext_clk_o(),
+      .pll_ctrl        (pll_ctrl)
+  );
+
+  initial begin
+    rst_n_i      = 1'b0;
+    f_past_valid = 1'b0;
+  end
+
+  always_ff @(posedge clk_i) begin
+    rst_n_i      <= 1'b1;
+    f_past_valid <= 1'b1;
+  end
+
+endmodule

rtl/mini/formal/pll_rcu_formal_props.v

@@ -0,0 +1,84 @@
+// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
+// retroSoC is licensed under Mulan PSL v2.
+
+module pll_rcu_formal;
+
+  localparam [2:0] PLL_IDLE = 3'd0;
+  localparam [2:0] PLL_SAFE = 3'd1;
+  localparam [2:0] PLL_APPLY = 3'd2;
+  localparam [2:0] PLL_WAIT_LOCK = 3'd3;
+  localparam [2:0] PLL_SWITCH = 3'd4;
+  localparam [2:0] PLL_RESPOND = 3'd5;
+
+  (* anyseq *) (* gclk *)reg        clk_i;
+  wire       rst_n_i;
+  wire       f_past_valid;
+  wire       req_valid;
+  wire [2:0] req_sel;
+  wire       req_ready;
+  wire       rsp_valid;
+  wire       rsp_ready;
+  wire       pll_lock;
+  wire       pll_capable;
+  wire [2:0] state;
+  wire       pll_apply;
+  wire       select_ext_clk;
+  wire       active_valid;
+  wire       safe_clk;
+  wire       active_lock;
+  wire [1:0] error;
+
+  pll_rcu_formal_design u_design (
+      .clk_i         (clk_i),
+      .rst_n_i       (rst_n_i),
+      .f_past_valid  (f_past_valid),
+      .req_valid     (req_valid),
+      .req_sel       (req_sel),
+      .req_ready     (req_ready),
+      .rsp_valid     (rsp_valid),
+      .rsp_ready     (rsp_ready),
+      .pll_lock      (pll_lock),
+      .pll_capable   (pll_capable),
+      .state         (state),
+      .pll_apply     (pll_apply),
+      .select_ext_clk(select_ext_clk),
+      .active_valid  (active_valid),
+      .safe_clk      (safe_clk),
+      .active_lock   (active_lock),
+      .error         (error)
+  );
+
+  always @(posedge clk_i) begin
+    if (f_past_valid && $past(rst_n_i && req_valid && !req_ready)) begin
+      assume (req_valid);
+      assume (req_sel == $past(req_sel));
+    end
+
+    if (rst_n_i) begin
+      assert(!(state == PLL_SAFE || state == PLL_APPLY || state == PLL_WAIT_LOCK) ||
+             select_ext_clk);
+      assert (!pll_apply || state != PLL_IDLE && state != PLL_SAFE);
+      if (f_past_valid && $past(state == PLL_SAFE && !pll_capable)) begin
+        assert (state == PLL_RESPOND);
+        assert (safe_clk);
+        assert (!active_valid);
+        assert (error == 2'd1);
+      end
+      if (f_past_valid && $past(state == PLL_WAIT_LOCK && pll_lock)) begin
+        assert (state == PLL_SWITCH);
+        assert (active_valid);
+        assert (!safe_clk);
+        assert (active_lock);
+        assert (error == 2'd0);
+      end
+      if (f_past_valid && $past(state == PLL_SWITCH)) begin
+        assert (state == PLL_RESPOND);
+        assert (!select_ext_clk);
+      end
+      cover (state == PLL_SWITCH && active_valid && active_lock);
+      cover (state == PLL_RESPOND && error == 2'd1);
+      cover (state == PLL_RESPOND && error == 2'd2);
+    end
+  end
+
+endmodule

rtl/mini/formal/sysctrl_formal.sv

@@ -0,0 +1,115 @@
+// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
+// retroSoC is licensed under Mulan PSL v2.
+
+module sysctrl_formal_design (
+    input  logic        clk_i,
+    output logic        rst_n_i,
+    output logic        f_past_valid,
+    output logic        nmi_valid,
+    output logic [31:0] nmi_addr,
+    output logic [31:0] nmi_wdata,
+    output logic [ 3:0] nmi_wstrb,
+    output logic        nmi_ready,
+    output logic [ 7:0] ip_sel,
+    output logic [ 4:0] core_sel,
+    output logic [ 2:0] pll_cfg,
+    output logic        pll_req_valid,
+    output logic        pll_req_ready,
+    output logic        pll_busy,
+    output logic        pll_error,
+    output logic [ 1:0] pll_error_reason,
+    output logic        pll_rsp_valid,
+    output logic        fault_valid,
+    output logic [31:0] fault_addr,
+    output logic [ 3:0] fault_wstrb,
+    output logic        fault_reserved,
+    output logic        fault_pending,
+    output logic        fault_write,
+    output logic [ 1:0] fault_reason,
+    output logic [31:0] fault_addr_q,
+    output logic [31:0] fault_count
+);
+
+  nmi_if nmi ();
+  sysctrl_if sysctrl ();
+  pll_ctrl_if pll_ctrl ();
+
+  (* anyseq *)logic        f_nmi_valid;
+  (* anyseq *)logic [31:0] f_nmi_addr;
+  (* anyseq *)logic [31:0] f_nmi_wdata;
+  (* anyseq *)logic [ 3:0] f_nmi_wstrb;
+  (* anyseq *)logic [ 4:0] f_core_sel;
+  (* anyseq *)logic        f_pll_req_ready;
+  (* anyseq *)logic [ 2:0] f_pll_active_sel;
+  (* anyseq *)logic        f_pll_active_valid;
+  (* anyseq *)logic        f_pll_safe_clk;
+  (* anyseq *)logic        f_pll_lock;
+  (* anyseq *)logic [ 1:0] f_pll_rsp_error;
+  (* anyseq *)logic        f_pll_rsp_valid;
+  (* anyseq *)logic        f_pll_capable;
+  (* anyseq *)logic        f_fault_valid;
+  (* anyseq *)logic [31:0] f_fault_addr;
+  (* anyseq *)logic [ 3:0] f_fault_wstrb;
+  (* anyseq *)logic        f_fault_reserved;
+
+  assign nmi.valid                   = f_nmi_valid;
+  assign nmi.addr                    = f_nmi_addr;
+  assign nmi.wdata                   = f_nmi_wdata;
+  assign nmi.wstrb                   = f_nmi_wstrb;
+  assign sysctrl.core_sel_i          = f_core_sel;
+  assign pll_ctrl.req_ready_i        = f_pll_req_ready;
+  assign pll_ctrl.rsp_active_sel_i   = f_pll_active_sel;
+  assign pll_ctrl.rsp_active_valid_i = f_pll_active_valid;
+  assign pll_ctrl.rsp_safe_clk_i     = f_pll_safe_clk;
+  assign pll_ctrl.rsp_pll_lock_i     = f_pll_lock;
+  assign pll_ctrl.rsp_error_i        = f_pll_rsp_error;
+  assign pll_ctrl.rsp_valid_i        = f_pll_rsp_valid;
+  assign pll_ctrl.capable_i          = f_pll_capable;
+
+  assign nmi_valid                   = nmi.valid;
+  assign nmi_addr                    = nmi.addr;
+  assign nmi_wdata                   = nmi.wdata;
+  assign nmi_wstrb                   = nmi.wstrb;
+  assign nmi_ready                   = nmi.ready;
+  assign ip_sel                      = sysctrl.ip_sel_o;
+  assign core_sel                    = u_dut.s_sysctrl_coresel_q;
+  assign pll_cfg                     = u_dut.s_pll_cfg_q;
+  assign pll_req_valid               = pll_ctrl.req_valid_o;
+  assign pll_req_ready               = pll_ctrl.req_ready_i;
+  assign pll_busy                    = u_dut.s_pll_busy_q;
+  assign pll_error                   = u_dut.s_pll_error_q;
+  assign pll_error_reason            = u_dut.s_pll_error_reason_q;
+  assign pll_rsp_valid               = pll_ctrl.rsp_valid_i;
+  assign fault_valid                 = f_fault_valid;
+  assign fault_addr                  = f_fault_addr;
+  assign fault_wstrb                 = f_fault_wstrb;
+  assign fault_reserved              = f_fault_reserved;
+  assign fault_pending               = u_dut.s_fault_pending_q;
+  assign fault_write                 = u_dut.s_fault_write_q;
+  assign fault_reason                = u_dut.s_fault_reason_q;
+  assign fault_addr_q                = u_dut.s_fault_addr_q;
+  assign fault_count                 = u_dut.s_fault_count_q;
+
+  nmi_sysctrl u_dut (
+      .clk_i           (clk_i),
+      .rst_n_i         (rst_n_i),
+      .fault_valid_i   (f_fault_valid),
+      .fault_addr_i    (f_fault_addr),
+      .fault_wstrb_i   (f_fault_wstrb),
+      .fault_reserved_i(f_fault_reserved),
+      .nmi             (nmi),
+      .sysctrl         (sysctrl),
+      .pll_ctrl        (pll_ctrl)
+  );
+
+  initial begin
+    rst_n_i      = 1'b0;
+    f_past_valid = 1'b0;
+  end
+
+  always_ff @(posedge clk_i) begin
+    rst_n_i      <= 1'b1;
+    f_past_valid <= 1'b1;
+  end
+
+endmodule

rtl/mini/formal/sysctrl_formal_props.v

@@ -0,0 +1,130 @@
+// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
+// retroSoC is licensed under Mulan PSL v2.
+
+module sysctrl_formal;
+
+  localparam [7:0] SYSCTRL_IPSEL_OFFSET = 8'h04;
+  localparam [7:0] SYSCTRL_PLL_CFG_OFFSET = 8'h08;
+  localparam [7:0] SYSCTRL_PLL_CMD_OFFSET = 8'h0c;
+  localparam [7:0] SYSCTRL_FAULT_STATUS_OFFSET = 8'h10;
+
+  (* anyseq *) (* gclk *)reg         clk_i;
+  wire        rst_n_i;
+  wire        f_past_valid;
+  wire        nmi_valid;
+  wire [31:0] nmi_addr;
+  wire [31:0] nmi_wdata;
+  wire [ 3:0] nmi_wstrb;
+  wire        nmi_ready;
+  wire [ 7:0] ip_sel;
+  wire [ 4:0] core_sel;
+  wire [ 2:0] pll_cfg;
+  wire        pll_req_valid;
+  wire        pll_req_ready;
+  wire        pll_busy;
+  wire        pll_error;
+  wire [ 1:0] pll_error_reason;
+  wire        pll_rsp_valid;
+  wire        fault_valid;
+  wire [31:0] fault_addr;
+  wire [ 3:0] fault_wstrb;
+  wire        fault_reserved;
+  wire        fault_pending;
+  wire        fault_write;
+  wire [ 1:0] fault_reason;
+  wire [31:0] fault_addr_q;
+  wire [31:0] fault_count;
+
+  sysctrl_formal_design u_design (
+      .clk_i           (clk_i),
+      .rst_n_i         (rst_n_i),
+      .f_past_valid    (f_past_valid),
+      .nmi_valid       (nmi_valid),
+      .nmi_addr        (nmi_addr),
+      .nmi_wdata       (nmi_wdata),
+      .nmi_wstrb       (nmi_wstrb),
+      .nmi_ready       (nmi_ready),
+      .ip_sel          (ip_sel),
+      .core_sel        (core_sel),
+      .pll_cfg         (pll_cfg),
+      .pll_req_valid   (pll_req_valid),
+      .pll_req_ready   (pll_req_ready),
+      .pll_busy        (pll_busy),
+      .pll_error       (pll_error),
+      .pll_error_reason(pll_error_reason),
+      .pll_rsp_valid   (pll_rsp_valid),
+      .fault_valid     (fault_valid),
+      .fault_addr      (fault_addr),
+      .fault_wstrb     (fault_wstrb),
+      .fault_reserved  (fault_reserved),
+      .fault_pending   (fault_pending),
+      .fault_write     (fault_write),
+      .fault_reason    (fault_reason),
+      .fault_addr_q    (fault_addr_q),
+      .fault_count     (fault_count)
+  );
+
+  always @(posedge clk_i) begin
+    if (f_past_valid && $past(rst_n_i && nmi_valid && !nmi_ready)) begin
+      assume (nmi_valid);
+      assume (nmi_addr == $past(nmi_addr));
+      assume (nmi_wdata == $past(nmi_wdata));
+      assume (nmi_wstrb == $past(nmi_wstrb));
+    end
+    if (rst_n_i && pll_rsp_valid) begin
+      assume (pll_busy);
+    end
+
+    if (rst_n_i && f_past_valid) begin
+      if ($past(
+              rst_n_i && nmi_valid && !nmi_ready && |nmi_wstrb &&
+                nmi_addr[7:0] == SYSCTRL_IPSEL_OFFSET
+          )) begin
+        assert (ip_sel == $past(nmi_wdata[7:0]));
+      end
+      if ($past(
+              rst_n_i && nmi_valid && !nmi_ready && nmi_wstrb[0] &&
+                nmi_addr[7:0] == SYSCTRL_PLL_CFG_OFFSET
+          )) begin
+        assert (pll_cfg == $past(nmi_wdata[2:0]));
+      end
+      if ($past(
+              rst_n_i && nmi_valid && !nmi_ready && nmi_wstrb[0] && nmi_wdata[0] &&
+                nmi_addr[7:0] == SYSCTRL_PLL_CMD_OFFSET && !pll_busy && !pll_req_valid
+          )) begin
+        assert (pll_busy);
+      end
+      if ($past(
+              rst_n_i && nmi_valid && !nmi_ready && nmi_wstrb[0] && nmi_wdata[0] &&
+                nmi_addr[7:0] == SYSCTRL_PLL_CMD_OFFSET && pll_busy
+          )) begin
+        assert (pll_error);
+        if (!$past(pll_rsp_valid)) begin
+          assert (pll_error_reason == 2'd3);
+        end
+      end
+      if ($past(rst_n_i && fault_valid)) begin
+        assert (fault_pending);
+        assert (fault_write == (|$past(fault_wstrb)));
+        assert (fault_reason == ($past(fault_reserved) ? 2'd2 : 2'd1));
+        assert (fault_addr_q == $past(fault_addr));
+        if (!$past(&fault_count)) begin
+          assert (fault_count == $past(fault_count) + 32'd1);
+        end
+      end
+      if ($past(
+              rst_n_i && nmi_valid && !nmi_ready && nmi_wstrb[0] && nmi_wdata[0] &&
+                nmi_addr[7:0] == SYSCTRL_FAULT_STATUS_OFFSET && !fault_valid
+          )) begin
+        assert (!fault_pending);
+      end
+    end
+
+    if (rst_n_i) begin
+      cover (pll_busy && pll_req_valid);
+      cover (pll_error && pll_error_reason == 2'd3);
+      cover (fault_pending && fault_reason == 2'd2);
+    end
+  end
+
+endmodule

rtl/mini/mk/formal.mk

@@ -6,7 +6,7 @@ FORMAL_SOLVER_DIR         := $(FORMAL_DIR)/bin
 FORMAL_SOLVER_WRAPPER     := $(FORMAL_SOLVER_DIR)/bitwuzla
 FORMAL_DEPTH              ?= 20
 FORMAL_TIMEOUT            ?= 60
-FORMAL_TARGETS            := bus nmi2apb
+FORMAL_TARGETS            := bus nmi2apb sysctrl pll_rcu gpio_mdd
 FORMAL_FILELIST_GENERATOR := $(RTL_PATH)/formal/generate_formal_filelist.py
 FORMAL_SBY_GENERATOR      := $(RTL_PATH)/formal/generate_sby_config.py
 FORMAL_RESULT_GENERATOR   := $(RTL_PATH)/formal/formal_results.py
@@ -14,11 +14,23 @@ FORMAL_SOURCE_FILES       := $(RTL_PATH)/formal/bus_formal.sv \
                              $(RTL_PATH)/formal/bus_formal_props.v \
                              $(RTL_PATH)/formal/nmi2apb_formal.sv \
                              $(RTL_PATH)/formal/nmi2apb_formal_props.v \
+                             $(RTL_PATH)/formal/sysctrl_formal.sv \
+                             $(RTL_PATH)/formal/sysctrl_formal_props.v \
+                             $(RTL_PATH)/formal/pll_rcu_formal.sv \
+                             $(RTL_PATH)/formal/pll_rcu_formal_props.v \
+                             $(RTL_PATH)/formal/gpio_mdd_formal.sv \
+                             $(RTL_PATH)/formal/gpio_mdd_formal_props.v \
                              $(RTL_PATH)/top/bus.sv \
                              $(ROOT_PATH)/rtl/ip/native/interconnect/nmi2apb.sv \
                              $(ROOT_PATH)/rtl/ip/native/interconnect/nmi_regslice.sv \
+                             $(ROOT_PATH)/rtl/ip/native/peripheral/gpio.sv \
+                             $(ROOT_PATH)/rtl/ip/native/peripheral/pll_ctrl_if.sv \
+                             $(ROOT_PATH)/rtl/ip/native/peripheral/sysctrl.sv \
+                             $(RTL_PATH)/top/rcu.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/interface/nmi_if.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/interface/apb4_pure_if.sv \
+                             $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_sync.sv \
+                             $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_2phase.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/edge_det.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/register.sv \
                              $(ROOT_PATH)/scripts/bitwuzla_smt2.py
@@ -94,10 +106,16 @@ formal-bus: $(FORMAL_DIR)/bus/.stamp | manifest
 
 formal-nmi2apb: $(FORMAL_DIR)/nmi2apb/.stamp | manifest
 
+formal-sysctrl: $(FORMAL_DIR)/sysctrl/.stamp | manifest
+
+formal-pll-rcu: $(FORMAL_DIR)/pll_rcu/.stamp | manifest
+
+formal-gpio-mdd: $(FORMAL_DIR)/gpio_mdd/.stamp | manifest
+
 formal-doctor:
 	$(MAKE) FORMAL=YES SIMU=IVERILOG SYNTH=YOSYS STA=NONE doctor
 
 formal-clean:
 	python3 $(ROOT_PATH)/scripts/clean.py --root $(ROOT_PATH) --path $(FORMAL_DIR)
 
-.PHONY: formal formal-bus formal-nmi2apb formal-doctor formal-clean
+.PHONY: formal formal-bus formal-nmi2apb formal-sysctrl formal-pll-rcu formal-gpio-mdd formal-doctor formal-clean

scripts/README.md

@@ -8,6 +8,11 @@ Scripts are part of the build contract. Prefer existing helpers over ad-hoc
 shell behavior, preserve structured JSON results, and keep setup/download
 behavior controlled by `config/dependencies.lock.json`.
 
+`publish_fatfs_artifact.sh` is the manual release helper for the lock-pinned
+FatFs R0.16 archive. It verifies the archive, GitHub authentication, release
+absence, and the published asset checksum before reporting the checksum-pinned
+URL.
+
 Update or add tests in [`../tests`](../tests) for script behavior. Run
 `ruff check .` and `python3 -m pytest -q`; build-flow changes also require the
 relevant dry-run or regression profile from [`AGENTS.md`](../AGENTS.md).

tests/test_script_tools.py

@@ -113,11 +113,20 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
 
     bus_filelist = tmp_path / "bus.fl"
     nmi2apb_filelist = tmp_path / "nmi2apb.fl"
+    sysctrl_filelist = tmp_path / "sysctrl.fl"
+    pll_rcu_filelist = tmp_path / "pll_rcu.fl"
+    gpio_mdd_filelist = tmp_path / "gpio_mdd.fl"
     assert generate_formal_filelist("bus", bus_filelist, memory_map, topology)
     assert generate_formal_filelist("nmi2apb", nmi2apb_filelist, memory_map, topology)
+    assert generate_formal_filelist("sysctrl", sysctrl_filelist, memory_map, topology)
+    assert generate_formal_filelist("pll_rcu", pll_rcu_filelist, memory_map, topology)
+    assert generate_formal_filelist("gpio_mdd", gpio_mdd_filelist, memory_map, topology)
 
-    bus = parse_filelists([bus_filelist])
-    nmi2apb = parse_filelists([nmi2apb_filelist])
+    bus = parse_filelists([bus_filelist], require_files=False)
+    nmi2apb = parse_filelists([nmi2apb_filelist], require_files=False)
+    sysctrl = parse_filelists([sysctrl_filelist], require_files=False)
+    pll_rcu = parse_filelists([pll_rcu_filelist], require_files=False)
+    gpio_mdd = parse_filelists([gpio_mdd_filelist], require_files=False)
     assert "+define+SV_ASSRT_DISABLE" in bus.defines
     assert ROOT / "rtl/mini/top/bus.sv" in bus.files
     assert ROOT / "rtl/ip/native/interconnect/nmi_regslice.sv" in bus.files
@@ -125,6 +134,15 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
     assert ROOT / "rtl/ip/native/interconnect/nmi2apb.sv" in nmi2apb.files
     assert ROOT / "rtl/mini/formal/nmi2apb_formal.sv" in nmi2apb.files
     assert ROOT / "rtl/managed/clusterip/common/rtl/interface/apb4_pure_if.sv" in nmi2apb.files
+    assert ROOT / "rtl/ip/native/peripheral/sysctrl.sv" in sysctrl.files
+    assert ROOT / "rtl/mini/formal/sysctrl_formal.sv" in sysctrl.files
+    assert ROOT / "rtl/mini/top/rcu.sv" in pll_rcu.files
+    assert ROOT / "rtl/managed/clusterip/common/rtl/cdc/cdc_2phase.sv" in pll_rcu.files
+    assert ROOT / "rtl/ip/native/peripheral/gpio.sv" in gpio_mdd.files
+    assert ROOT / "rtl/managed/clusterip/common/rtl/cdc/cdc_sync.sv" in gpio_mdd.files
+    assert ROOT / "rtl/mini/formal/gpio_mdd_formal.sv" in gpio_mdd.files
+    assert "+define+IP_MDD" in gpio_mdd.defines
+    assert "+define+IP_MDD" not in sysctrl.defines
 
 
 def test_sby_config_uses_prove_and_cover_with_bitwuzla(tmp_path: Path) -> None:
@@ -145,8 +163,20 @@ def test_bitwuzla_wrapper_translates_yosys_legacy_arguments() -> None:
     assert translate_arguments(["--smt2", "-i", "--seed=1"]) == ["--lang", "smt2", "--seed=1"]
 
 
+def test_fatfs_release_script_uses_the_locked_archive_contract() -> None:
+    script = ROOT / "scripts/publish_fatfs_artifact.sh"
+    content = script.read_text(encoding="utf-8")
+
+    assert script.stat().st_mode & 0o111
+    assert 'readonly RELEASE_TAG="fatfs-r0.16"' in content
+    assert 'readonly ASSET_NAME="fatfs-r0.16.zip"' in content
+    assert "99f7dc1f7e095356e4a9e3dbe29959090d8b948afe2bbc5441e52fdf4b85449e" in content
+    assert 'gh release download "$RELEASE_TAG"' in content
+
+
 def test_formal_result_summary_requires_every_passing_step(tmp_path: Path) -> None:
-    for proof in ("bus", "nmi2apb"):
+    proofs = ("bus", "nmi2apb", "sysctrl", "pll_rcu", "gpio_mdd")
+    for proof in proofs:
         directory = tmp_path / proof
         directory.mkdir()
         for step in ("sv2v", "prove", "cover"):
@@ -168,10 +198,16 @@ def test_formal_result_summary_requires_every_passing_step(tmp_path: Path) -> No
         f"bus={tmp_path / 'bus'}",
         "--proof",
         f"nmi2apb={tmp_path / 'nmi2apb'}",
+        "--proof",
+        f"sysctrl={tmp_path / 'sysctrl'}",
+        "--proof",
+        f"pll_rcu={tmp_path / 'pll_rcu'}",
+        "--proof",
+        f"gpio_mdd={tmp_path / 'gpio_mdd'}",
     )
     result = json.loads(output.read_text(encoding="utf-8"))
     assert result["status"] == "passed"
-    assert set(result["proofs"]) == {"bus", "nmi2apb"}
+    assert set(result["proofs"]) == set(proofs)
 
 
 def test_legacy_user_gpio_interface_is_migrated_in_generated_source(tmp_path: Path) -> None: