feat: update nmi2apb formal design and properties for user IP integration

- Expanded psel_comb and psel_q to 10 bits in nmi2apb_formal.sv and nmi2apb_formal_props.v.
- Added user_ip interface and corresponding formal slave instance in nmi2apb_formal_design.
- Implemented migration of legacy user-extension includes to user_extensions.svh in generate_mpw.py.
- Enhanced configured_filelist function to accept require_files parameter in export_soc_sources.py.
- Updated tests to validate user extension migration and formal design changes.

rtl/mini/formal/nmi2apb_formal.sv

@@ -31,8 +31,8 @@ module nmi2apb_formal_design (
     output logic [31:0] nmi_wdata,
     output logic [ 3:0] nmi_wstrb,
     output logic        nmi_ready,
-    output logic [ 8:0] psel_comb,
-    output logic [ 8:0] psel_q,
+    output logic [ 9:0] psel_comb,
+    output logic [ 9:0] psel_q,
     output logic        xfer_ready,
     output logic [ 1:0] fsm_q
 );
@@ -47,6 +47,7 @@ module nmi2apb_formal_design (
   apb4_pure_if wdg ();
   apb4_pure_if crc ();
   apb4_pure_if tmr ();
+  apb4_pure_if user_ip ();
 
   (* anyseq *)logic        f_nmi_valid;
   (* anyseq *)logic [31:0] f_nmi_addr;
@@ -72,6 +73,7 @@ module nmi2apb_formal_design (
   formal_apb_slave u_wdg_slave (.apb(wdg));
   formal_apb_slave u_crc_slave (.apb(crc));
   formal_apb_slave u_tmr_slave (.apb(tmr));
+  formal_apb_slave u_user_ip_slave (.apb(user_ip));
 
   nmi2apb u_dut (
       .clk_i   (clk_i),
@@ -85,7 +87,8 @@ module nmi2apb_formal_design (
       .rtc     (rtc),
       .wdg     (wdg),
       .crc     (crc),
-      .tmr     (tmr)
+      .tmr     (tmr),
+      .user_ip (user_ip)
   );
 
   assign psel_comb  = u_dut.s_psel_comb;

rtl/mini/formal/nmi2apb_formal_props.v

@@ -21,8 +21,8 @@ module nmi2apb_formal;
   wire [31:0] nmi_wdata;
   wire [ 3:0] nmi_wstrb;
   wire        nmi_ready;
-  wire [ 8:0] psel_comb;
-  wire [ 8:0] psel_q;
+  wire [ 9:0] psel_comb;
+  wire [ 9:0] psel_q;
   wire        xfer_ready;
   wire [ 1:0] fsm_q;
 

scripts/generate_mpw.py

@@ -53,6 +53,20 @@ def rewrite_filelists(root: Path, replacements: tuple[tuple[Path, Path], ...]) -
         filelist.write_text(content, encoding="utf-8")
 
 
+def migrate_user_extension_includes(root: Path) -> list[Path]:
+    """Migrate legacy user-extension includes in isolated MPW sources."""
+    legacy_include = re.compile(r'`include\s+"mdd_config\.svh"')
+    migrated: list[Path] = []
+    for source in sorted(root.rglob("*.sv")):
+        content = source.read_text(encoding="utf-8")
+        content, replacements = legacy_include.subn('`include "user_extensions.svh"', content)
+        if replacements == 0:
+            continue
+        source.write_text(content, encoding="utf-8")
+        migrated.append(source)
+    return migrated
+
+
 def migrate_user_gpio_interfaces(root: Path) -> list[Path]:
     """Migrate legacy MPW user-IP GPIO ports in isolated build sources."""
     legacy_port = re.compile(r"\bgpio_if\.dut\s+gpio\b")
@@ -154,8 +168,10 @@ def generate(args: argparse.Namespace) -> None:
         run(workspace, log, mpw / "ip.py")
         run(workspace, log, mpw / "info.py", "IP")
         shutil.copytree(shared / "ip", candidate / "ip")
-        migrated = migrate_user_gpio_interfaces(candidate / "ip")
-        log.write(f"migrated user GPIO interfaces: {len(migrated)}\n")
+        migrated_includes = migrate_user_extension_includes(candidate / "ip")
+        migrated_gpio = migrate_user_gpio_interfaces(candidate / "ip")
+        log.write(f"migrated user-extension includes: {len(migrated_includes)}\n")
+        log.write(f"migrated user GPIO interfaces: {len(migrated_gpio)}\n")
         run(workspace, log, mpw / "core.py", args.simu)
         run(workspace, log, mpw / "info.py", "CORE")
         shutil.copytree(shared / "core", candidate / "core")

syn/tools/export_soc_sources.py

@@ -44,7 +44,11 @@ def build_defines(args: argparse.Namespace) -> list[str]:
 
 
 def configured_filelist(
-    args: argparse.Namespace, generated_dir: Path, user_extensions_dir: Path
+    args: argparse.Namespace,
+    generated_dir: Path,
+    user_extensions_dir: Path,
+    *,
+    require_files: bool = True,
 ) -> FileList:
     names = [
         "def.fl",
@@ -67,7 +71,7 @@ def configured_filelist(
     names.append(str(user_extensions_dir / "user_extensions.fl"))
     names.append("top.fl")
     paths = [Path(name) if Path(name).is_absolute() else generated_dir / name for name in names]
-    return parse_filelists(paths)
+    return parse_filelists(paths, require_files=require_files)
 
 
 def resolve_include(name: str, incdirs: list[Path], current_file: Path) -> Path | None:

tests/test_script_tools.py

@@ -32,6 +32,7 @@ from scripts.check_c_warnings import self_owned_warnings  # noqa: E402
 from scripts.check_format import format_files  # noqa: E402
 from scripts.dependency_lock import LockError, load_lock  # noqa: E402
 from scripts.generate_mpw import (  # noqa: E402
+    migrate_user_extension_includes,
     migrate_user_gpio_interfaces,
     remove_legacy_picorv32_entry,
 )
@@ -144,7 +145,9 @@ def test_source_export_selects_the_requested_management_core(tmp_path: Path) ->
         source_export.generate_user_extensions(
             ROOT / "rtl/mini/integration/user_extensions.json", user_extensions_dir
         )
-        filelist = source_export.configured_filelist(arguments, generated_dir, user_extensions_dir)
+        filelist = source_export.configured_filelist(
+            arguments, generated_dir, user_extensions_dir, require_files=False
+        )
 
         assert f"+define+CORE_{core}" in filelist.defines
         assert any(path.name == source_name for path in filelist.files)
@@ -273,7 +276,7 @@ def test_formal_result_summary_requires_every_passing_step(tmp_path: Path) -> No
 def test_legacy_user_gpio_interface_is_migrated_in_generated_source(tmp_path: Path) -> None:
     source = tmp_path / "user_ip_design.sv"
     source.write_text(
-        """`include "user_extensions.svh"
+        """`include "mdd_config.svh"
 module user_ip_design (gpio_if.dut gpio);
   logic value;
   assign gpio.gpio_oe = value;
@@ -287,6 +290,7 @@ endmodule
         encoding="utf-8",
     )
 
+    assert migrate_user_extension_includes(tmp_path) == [source]
     assert migrate_user_gpio_interfaces(tmp_path) == [source]
 
     migrated = source.read_text(encoding="utf-8")

tests/test_soc_topology.py

@@ -141,10 +141,18 @@ def test_topology_always_adds_the_user_apb_target(tmp_path: Path) -> None:
     interfaces = (tmp_path / "rtl/soc_apb_interfaces.svh").read_text(encoding="utf-8")
     declarations = (tmp_path / "rtl/soc_apb_declarations.svh").read_text(encoding="utf-8")
     response = (tmp_path / "rtl/soc_apb_response_mux.svh").read_text(encoding="utf-8")
+    formal_design = (ROOT / "rtl/mini/formal/nmi2apb_formal.sv").read_text(encoding="utf-8")
+    formal_properties = (ROOT / "rtl/mini/formal/nmi2apb_formal_props.v").read_text(
+        encoding="utf-8"
+    )
 
     assert "apb4_if u_user_ip_apb_if (clk_i, rst_n_i);" in interfaces
     assert "localparam int NSLV = 10;" in declarations
     assert "s_psel_q[9]" in response
+    assert "apb4_pure_if user_ip ();" in formal_design
+    assert ".user_ip (user_ip)" in formal_design
+    assert "logic [ 9:0] psel_comb" in formal_design
+    assert "wire [ 9:0] psel_comb" in formal_properties
 
 
 def test_topology_rejects_unknown_or_non_native_regions(tmp_path: Path) -> None: