feat: add formal properties for sysctrl and update related files

- Introduced  to define formal properties for the sysctrl module.
- Updated  to include new formal properties and source files.
- Renamed  to  in the bus module and created a new  file.
- Implemented a testbench for  in .
- Removed the obsolete  test file.
- Updated test scripts to reference the new  instead of the old RAM module.
- Adjusted various test files to ensure compatibility with the new structure and naming conventions.

Makefile

@@ -210,7 +210,7 @@ endif
 	benchmark-report \
 	pin-map check-pin-map soc-topology check-soc-topology user-extensions check-user-extensions \
 	check-clock-reset-domains tech-cell-test rtl-lint check-rtl-lint \
-	formal formal-bus formal-rib-adapter formal-spill-register formal-ribp2apb formal-clean formal-doctor
+	formal formal-bus formal-rib-adapter formal-ribp2apb formal-clean formal-doctor
 .NOTPARALLEL: setup
 
 help:
@@ -235,7 +235,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-rib-adapter | formal-spill-register | formal-ribp2apb run SBY protocol proofs' \
+	  '  formal | formal-bus | formal-rib-adapter | formal-ribp2apb run SBY protocol proofs' \
 	  '  formal-sysctrl | formal-pll-rcu | formal-gpio-user run SBY peripheral-control proofs' \
 	  '  formal-doctor              check the SBY, Yosys, sv2v, and Bitwuzla formal toolchain' \
 	  '  benchmark-report           run the benchmark profile and write meta/performance.json' \

docs/engineering.md

@@ -111,16 +111,15 @@ Verilator regressions.
 
 `make CONFIG=configs/ci/ihp130.mk formal` proves selected
 protocol invariants with SymbiYosys, Yosys, `sv2v`, and Bitwuzla. The current
-targets are `bus`, `rib_adapter`, `spill_register`, `ribp2apb`, `sysctrl`,
-`pll_rcu`, and `gpio_user`; each uses
+targets are `bus`, `rib_adapter`, `ribp2apb`, `sysctrl`, `pll_rcu`, and
+`gpio_user`; 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_user` checks fixed user-GPIO ownership, lock, handoff,
 and mux safety. `rib_adapter` checks both single-word compatibility adapters
-under backpressure. `spill_register` checks the externally visible occupancy,
-ready/valid, flush, and stalled-output contract of the common response buffer;
-its deterministic simulation scoreboard separately checks data ordering.
+under backpressure. Direct Common utility proofs, including `spill_register`,
+are maintained in the Common repository.
 `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.

docs/rib-interconnect.md

@@ -1,39 +1,74 @@
-# RIB Interconnect Protocol
+# RIB Family Protocols
 
-RIB is the retroSoC Interconnect Bus. The SoC-owned version 1 transport uses
-separate command, write-data, and response channels. It supports one
-outstanding 32-bit transaction per master and two linear lengths:
+retroSoC uses three related protocols. The interface declarations and the
+generated address map are the executable source of truth; this document fixes
+the ownership, ordering, and adaptation rules at each boundary.
 
-- `INCR1` transfers one word.
-- `INCR4` transfers four words at `address + 0`, `+4`, `+8`, and `+12`.
+| Protocol | Interface | Purpose | Transfer shape |
+| --- | --- | --- | --- |
+| RIBL | `soc_ribl_if` | Legacy SoC master compatibility | One scalar word request and response |
+| RIB | `soc_rib_if` | Native retroSoC interconnect | Split command, write-data, and response channels |
+| RIBP | ClusterIP `ribp_if` | Peripheral and IP compatibility | One scalar word request and response |
 
-`INCR4` commands must be 16-byte aligned. They may not cross a generated
-address-map capability boundary. There are no IDs, wrapping bursts, narrow
-read beats, reordering, or multiple outstanding transactions in version 1.
-The response carries a beat index, terminal marker, error flag, and response
-code. `BURSTERR` reports an unsupported length, bad alignment, unsupported
-target, or malformed write-last sequence.
+## RIBL
+
+RIBL is the SoC-owned scalar compatibility protocol. A master presents
+`valid`, `addr`, `wdata`, and `wstrb`; a slave completes the request with
+`ready`, `rdata`, and `resp_err`. `wstrb == 0` denotes a read. There is no
+burst metadata, response code, ID, reordering, or more than one transaction
+in flight through the RIBL adapter.
+
+`soc_ribl2rib` converts RIBL requests to native `INCR1` RIB transactions. It
+maps the terminal RIB response to the RIBL `ready` handshake and propagates
+the RIB error flag as `resp_err`.
+
+## RIB
+
+RIB is the retroSoC Interconnect Bus. Version 1 has independent command,
+write-data, and response channels and permits one outstanding 32-bit
+transaction per master.
+
+- A command transfers `cmd_addr`, `cmd_write`, and `cmd_len` with
+  `cmd_valid/cmd_ready`.
+- Write beats transfer `wdata`, `wstrb`, and `wlast` with `w_valid/w_ready`.
+- Responses transfer `rdata`, `resp_err`, `resp_code`, `rsp_beat`, and
+  `rsp_last` with `rsp_valid/rsp_ready`.
+- `INCR1` transfers one word. `INCR4` transfers four ascending words at
+  `address + 0`, `+4`, `+8`, and `+12` and requires a 16-byte aligned address.
+
+RIB has no IDs, narrow read beats, wrapping bursts, reordering, or multiple
+outstanding transactions. `BURSTERR` reports an unsupported length, bad
+alignment, unsupported target, or malformed write-last sequence. The response
+code definitions are in `soc_rib_defs.svh`.
 
 The generated address map is the capability source of truth. Register and APB
 regions remain `INCR1` only. SRAM, SDRAM, PSRAM, flash/XPI, and SPI-SD memory
 windows accept `INCR4`; the interconnect validates both the first and last
-address before forwarding a command. A DMA transfer falls back to `INCR1`
-unless both endpoints, including their fourth words, support `INCR4`.
+address before forwarding a command. DMA falls back to `INCR1` unless both
+endpoints, including their fourth words, support `INCR4`.
 
-## Compatibility and Performance
+## RIBP
 
-The management core and the currently integrated user cores retain their
-single-word interfaces through SoC-owned legacy-to-burst adapters. A future
-user core can select the burst interface in `user_extensions.json`. DMA is a
-native burst master and uses the common four-entry FIFO for each chunk.
+RIBP is the scalar ClusterIP protocol defined by `ribp_if`. It transfers
+`addr`, `wdata`, and `wstrb` with `valid/ready`; `wstrb == 0` denotes a read
+and `rdata` is returned with the completing `ready` handshake. RIBP carries no
+burst length, beat index, terminal marker, response code, or error signal.
 
-The SRAM target is native burst RTL. It pipelines synchronous reads and uses
-the common two-entry spill register to absorb response backpressure. The spill
-register contract assumes that `flush_i` and `valid_i` are not asserted
-together. When both entries are full it does not accept a replacement item in
-the same cycle as a downstream pop, so recovery from a full stall contains one
-refill bubble. This does not affect the no-bubble four-beat path when the
-response consumer remains ready.
+`soc_rib2ribp` serializes legal RIB beats into RIBP accesses and reconstructs
+ordered RIB responses. Target-side error sideband inputs are converted to RIB
+response status at this boundary. `ribp2rib` is the inverse compatibility
+adapter for a scalar RIBP initiator that must access a native RIB target.
+
+## Targets and Performance
+
+Management and current user cores use RIBL through the SoC adapters. Future
+user cores can select native RIB in `user_extensions.json`. DMA is a native
+RIB master and uses the common four-entry FIFO for each chunk.
+
+`soc_rib2ram` is the native RIB SRAM target. It pipelines synchronous reads
+and uses the Common two-entry spill register for response backpressure. The
+Common repository owns direct verification of that utility; retroSoC verifies
+the RIB target behavior and its integration contract.
 
 The current external-memory boundary accepts one `INCR4` command and converts
 it into ordered legacy word accesses. This reduces upstream command and
@@ -52,12 +87,10 @@ and error termination.
 
 ## Verification
 
-`make CONFIG=configs/ci/ihp130.mk FORMAL=YES formal` checks the arbiter and both
-compatibility adapters. It also proves the common spill register's externally
-observable occupancy, ready/valid, flush, and stalled-output contracts. The
-deterministic Icarus scoreboard additionally checks spill-register data order,
-and the SRAM test covers INCR4 reads, writes, no-bubble responses, and prolonged
-backpressure.
+`make CONFIG=configs/ci/ihp130.mk FORMAL=YES formal` checks the arbiter and
+both compatibility adapters. The SRAM test covers INCR4 reads, writes,
+no-bubble responses, and prolonged backpressure. Direct spill-register
+simulation and formal coverage is maintained by the Common repository.
 
 The `APP=benchmark` UART records include `cycles` and interconnect wait
 counters. `make CONFIG=configs/benchmark/ihp130-hazard3.mk SIMU=VERILATOR

rtl/mini/filelist/top.fl

@@ -4,7 +4,7 @@
 /top/ribp2rib.sv
 /top/soc_rib2ribp.sv
 /top/soc_rib_error_slave.sv
-/top/soc_rib_ram.sv
+/top/soc_rib2ram.sv
 /top/core_wrapper.sv
 /top/retrosoc.sv
 /top/retrosoc_asic.sv

rtl/mini/formal/generate_formal_filelist.py

@@ -41,7 +41,7 @@ def source_files(target: str) -> list[Path]:
             TOP / "soc_ribl2rib.sv",
             TOP / "soc_rib2ribp.sv",
             TOP / "soc_rib_error_slave.sv",
-            TOP / "soc_rib_ram.sv",
+            TOP / "soc_rib2ram.sv",
             TOP / "bus.sv",
             SCRIPT_DIR / "bus_formal.sv",
         ]
@@ -52,12 +52,6 @@ def source_files(target: str) -> list[Path]:
             TOP / "soc_rib2ribp.sv",
             SCRIPT_DIR / "rib_adapter_formal.sv",
         ]
-    if target == "spill_register":
-        return [
-            *common,
-            COMMON_RTL / "utils/spill_register.sv",
-            SCRIPT_DIR / "spill_register_formal.sv",
-        ]
     if target == "ribp2apb":
         return [
             COMMON_RTL / "interface/ribp_if.sv",
@@ -80,6 +74,7 @@ def source_files(target: str) -> list[Path]:
             COMMON_RTL / "cdc/cdc_sync.sv",
             COMMON_RTL / "cdc/cdc_rst_ctrlr.sv",
             COMMON_RTL / "cdc/cdc_2phase.sv",
+            COMMON_RTL / "clkrst/rst_sync.sv",
             PERIPHERAL / "pll_ctrl_if.sv",
             TOP / "rcu.sv",
             SCRIPT_DIR / "pll_rcu_formal.sv",
@@ -128,7 +123,6 @@ def parse_args() -> argparse.Namespace:
         choices=(
             "bus",
             "rib_adapter",
-            "spill_register",
             "ribp2apb",
             "sysctrl",
             "pll_rcu",

rtl/mini/formal/pll_rcu_formal.sv

@@ -18,6 +18,7 @@ module pll_rcu_formal_design (
     output logic       active_valid,
     output logic       safe_clk,
     output logic       active_lock,
+    output logic       lock_seen_low,
     output logic [1:0] error
 );
 
@@ -45,6 +46,7 @@ module pll_rcu_formal_design (
   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 lock_seen_low        = u_dut.s_lock_seen_low_q;
   assign error                = u_dut.s_error_q;
 
   // Both controller domains share the formal clock. This proves the control

rtl/mini/formal/pll_rcu_formal_props.sv

@@ -26,6 +26,7 @@ module pll_rcu_formal;
   wire       active_valid;
   wire       safe_clk;
   wire       active_lock;
+  wire       lock_seen_low;
   wire [1:0] error;
 
   pll_rcu_formal_design u_design (
@@ -45,6 +46,7 @@ module pll_rcu_formal;
       .active_valid  (active_valid),
       .safe_clk      (safe_clk),
       .active_lock   (active_lock),
+      .lock_seen_low (lock_seen_low),
       .error         (error)
   );
 
@@ -64,7 +66,7 @@ module pll_rcu_formal;
         assert (!active_valid);
         assert (error == 2'd1);
       end
-      if (f_past_valid && $past(state == PLL_WAIT_LOCK && pll_lock)) begin
+      if (f_past_valid && $past(state == PLL_WAIT_LOCK && pll_lock && lock_seen_low)) begin
         assert (state == PLL_SWITCH);
         assert (active_valid);
         assert (!safe_clk);

rtl/mini/formal/spill_register_formal.sv

@@ -1,52 +0,0 @@
-// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
-// retroSoC is licensed under Mulan PSL v2.
-
-module spill_register_formal_design (
-    input  logic        clk_i,
-    output logic        rst_n_i,
-    output logic        f_past_valid,
-    output logic        flush_i,
-    output logic        valid_i,
-    output logic        ready_o,
-    output logic [31:0] data_i,
-    output logic        valid_o,
-    output logic        ready_i,
-    output logic [31:0] data_o
-);
-
-  (* anyseq *)logic        f_flush;
-  (* anyseq *)logic        f_valid;
-  (* anyseq *)logic [31:0] f_data;
-  (* anyseq *)logic        f_ready;
-
-  assign flush_i = f_flush;
-  assign valid_i = f_valid;
-  assign data_i  = f_data;
-  assign ready_i = f_ready;
-
-  spill_register #(
-      .DATA_WIDTH(32),
-      .BYPASS    (1'b0)
-  ) u_spill_register (
-      .clk_i  (clk_i),
-      .rst_n_i(rst_n_i),
-      .flush_i(flush_i),
-      .valid_i(valid_i),
-      .ready_o(ready_o),
-      .data_i (data_i),
-      .valid_o(valid_o),
-      .ready_i(ready_i),
-      .data_o (data_o)
-  );
-
-  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/spill_register_formal_props.v

@@ -1,64 +0,0 @@
-// Copyright (c) 2026 Yuchi Miao <miaoyuchi@ict.ac.cn>
-// retroSoC is licensed under Mulan PSL v2.
-
-module spill_register_formal;
-  (* anyseq *) (* gclk *)reg  clk_i;
-  wire rst_n_i;
-  wire f_past_valid;
-  wire flush_i, valid_i, ready_o, valid_o, ready_i;
-  wire [31:0] data_i, data_o;
-  reg  [1:0] count;
-
-  wire       push = valid_i && ready_o && !flush_i;
-  wire       pop = valid_o && ready_i && !flush_i;
-
-  spill_register_formal_design u_design (.*);
-
-  initial begin
-    count = 2'd0;
-  end
-
-  always @(posedge clk_i) begin
-    if (!rst_n_i) begin
-      count <= 2'd0;
-    end else begin
-      if (f_past_valid && $past(rst_n_i && valid_i && !ready_o)) begin
-        assume (valid_i);
-        assume (data_i == $past(data_i));
-      end
-
-      assert (count <= 2'd2);
-      assert (valid_o == (!flush_i && (count != 2'd0)));
-      assert (ready_o == (!flush_i && (count != 2'd2)));
-      if (flush_i) begin
-        assert (!valid_o);
-        assert (!ready_o);
-      end
-      if (f_past_valid && !flush_i && $past(rst_n_i && valid_o && !ready_i && !flush_i)) begin
-        assert (valid_o);
-        assert (data_o == $past(data_o));
-      end
-
-      if (flush_i) begin
-        count <= 2'd0;
-      end else begin
-        case ({
-          push, pop
-        })
-          2'b10: begin
-            count <= count + 1'b1;
-          end
-          2'b01: begin
-            count <= count - 1'b1;
-          end
-          2'b11:   count <= count;
-          default: count <= count;
-        endcase
-      end
-
-      cover (count == 2'd2 && !ready_i);
-      cover (f_past_valid && $past(count == 2'd2 && ready_i) && count == 2'd1);
-      cover (flush_i && count != 2'd0);
-    end
-  end
-endmodule

rtl/mini/mk/formal.mk

@@ -6,29 +6,27 @@ FORMAL_SOLVER_DIR         := $(FORMAL_DIR)/bin
 FORMAL_SOLVER_WRAPPER     := $(FORMAL_SOLVER_DIR)/bitwuzla
 FORMAL_DEPTH              ?= 20
 FORMAL_TIMEOUT            ?= 60
-FORMAL_TARGETS            := bus rib_adapter spill_register ribp2apb sysctrl pll_rcu gpio_user
+FORMAL_TARGETS            := bus rib_adapter ribp2apb sysctrl pll_rcu gpio_user
 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
 FORMAL_SOURCE_FILES       := $(RTL_PATH)/formal/bus_formal.sv \
-                             $(RTL_PATH)/formal/bus_formal_props.v \
+                             $(RTL_PATH)/formal/bus_formal_props.sv \
                              $(RTL_PATH)/formal/rib_adapter_formal.sv \
-                             $(RTL_PATH)/formal/rib_adapter_formal_props.v \
-                             $(RTL_PATH)/formal/spill_register_formal.sv \
-                             $(RTL_PATH)/formal/spill_register_formal_props.v \
+                             $(RTL_PATH)/formal/rib_adapter_formal_props.sv \
                              $(RTL_PATH)/formal/ribp2apb_formal.sv \
-                             $(RTL_PATH)/formal/ribp2apb_formal_props.v \
+                             $(RTL_PATH)/formal/ribp2apb_formal_props.sv \
                              $(RTL_PATH)/formal/sysctrl_formal.sv \
-                             $(RTL_PATH)/formal/sysctrl_formal_props.v \
+                             $(RTL_PATH)/formal/sysctrl_formal_props.sv \
                              $(RTL_PATH)/formal/pll_rcu_formal.sv \
-                             $(RTL_PATH)/formal/pll_rcu_formal_props.v \
+                             $(RTL_PATH)/formal/pll_rcu_formal_props.sv \
                              $(RTL_PATH)/formal/gpio_user_formal.sv \
-                             $(RTL_PATH)/formal/gpio_user_formal_props.v \
+                             $(RTL_PATH)/formal/gpio_user_formal_props.sv \
                              $(RTL_PATH)/top/bus.sv \
                              $(RTL_PATH)/top/soc_rib_error_slave.sv \
                              $(RTL_PATH)/top/soc_ribl_if.sv \
                              $(RTL_PATH)/top/soc_rib_if.sv \
-                             $(RTL_PATH)/top/soc_rib_ram.sv \
+                             $(RTL_PATH)/top/soc_rib2ram.sv \
                              $(RTL_PATH)/top/soc_rib2ribp.sv \
                              $(RTL_PATH)/top/soc_ribl2rib.sv \
                              $(ROOT_PATH)/rtl/ip/ribp/interconnect/ribp2apb.sv \
@@ -42,6 +40,7 @@ FORMAL_SOURCE_FILES       := $(RTL_PATH)/formal/bus_formal.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_sync.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_rst_ctrlr.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/cdc/cdc_2phase.sv \
+                             $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/clkrst/rst_sync.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/edge_det.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/register.sv \
                              $(ROOT_PATH)/rtl/managed/clusterip/common/rtl/utils/spill_register.sv \
@@ -69,16 +68,16 @@ $(FORMAL_DIR)/%/design.v: $(FORMAL_DIR)/%/formal.fl $(RTL_PATH)/script/convt_sv2
 		--log $(@D)/sv2v.log --result $(@D)/result-sv2v.json \
 		-- python3 $(RTL_PATH)/script/convt_sv2v.py -f $< --output $@
 
-$(FORMAL_DIR)/%/prove.sby: $(FORMAL_DIR)/%/design.v $(RTL_PATH)/formal/%_formal_props.v \
+$(FORMAL_DIR)/%/prove.sby: $(FORMAL_DIR)/%/design.v $(RTL_PATH)/formal/%_formal_props.sv \
 	$(FORMAL_SBY_GENERATOR)
 	python3 $(FORMAL_SBY_GENERATOR) --top $*_formal --input $< \
-		--properties $(RTL_PATH)/formal/$*_formal_props.v --solver $(FORMAL_SOLVER) \
+		--properties $(RTL_PATH)/formal/$*_formal_props.sv --solver $(FORMAL_SOLVER) \
 		--mode prove --depth $(FORMAL_DEPTH) --output $@
 
-$(FORMAL_DIR)/%/cover.sby: $(FORMAL_DIR)/%/design.v $(RTL_PATH)/formal/%_formal_props.v \
+$(FORMAL_DIR)/%/cover.sby: $(FORMAL_DIR)/%/design.v $(RTL_PATH)/formal/%_formal_props.sv \
 	$(FORMAL_SBY_GENERATOR)
 	python3 $(FORMAL_SBY_GENERATOR) --top $*_formal --input $< \
-		--properties $(RTL_PATH)/formal/$*_formal_props.v --solver $(FORMAL_SOLVER) \
+		--properties $(RTL_PATH)/formal/$*_formal_props.sv --solver $(FORMAL_SOLVER) \
 		--mode cover --depth $(FORMAL_DEPTH) --output $@
 
 $(FORMAL_SOLVER_WRAPPER): $(ROOT_PATH)/scripts/bitwuzla_smt2.py
@@ -119,8 +118,6 @@ formal-bus: $(FORMAL_DIR)/bus/.stamp | manifest
 
 formal-rib-adapter: $(FORMAL_DIR)/rib_adapter/.stamp | manifest
 
-formal-spill-register: $(FORMAL_DIR)/spill_register/.stamp | manifest
-
 formal-ribp2apb: $(FORMAL_DIR)/ribp2apb/.stamp | manifest
 
 formal-sysctrl: $(FORMAL_DIR)/sysctrl/.stamp | manifest
@@ -135,4 +132,4 @@ formal-doctor:
 formal-clean:
 	python3 $(ROOT_PATH)/scripts/clean.py --root $(ROOT_PATH) --path $(FORMAL_DIR)
 
-.PHONY: formal formal-bus formal-rib-adapter formal-spill-register formal-ribp2apb formal-sysctrl formal-pll-rcu formal-gpio-user formal-doctor formal-clean
+.PHONY: formal formal-bus formal-rib-adapter formal-ribp2apb formal-sysctrl formal-pll-rcu formal-gpio-user formal-doctor formal-clean

rtl/mini/top/bus.sv

@@ -115,7 +115,7 @@ module bus (
   );
 
 `ifdef HAVE_SRAM_IF
-  soc_rib_ram u_ram_slave (
+  soc_rib2ram u_rib2ram (
       .clk_i  (clk_i),
       .rst_n_i(rst_n_i),
       .rib    (u_ram_rib_if),

rtl/mini/top/soc_rib2ram.sv

@@ -10,7 +10,7 @@
 
 `include "soc_rib_defs.svh"
 
-module soc_rib_ram (
+module soc_rib2ram (
     input logic            clk_i,
     input logic            rst_n_i,
           soc_rib_if.slave rib,

scripts/check_format.py

@@ -18,6 +18,7 @@ SELF_OWNED_RTL_ROOTS = {
     ("rtl", "ip"),
     ("rtl", "mini"),
     ("rtl", "tech"),
+    ("tests", "rtl"),
 }
 
 
@@ -109,7 +110,11 @@ def main() -> int:
     args = parser.parse_args()
 
     root = args.root.resolve()
-    files = format_files(tracked_files(root), args.kind)
+    files = [
+        path
+        for path in format_files(tracked_files(root), args.kind)
+        if (root / path).is_file()
+    ]
     if not files:
         print(f"no tracked {args.kind} files selected")
         return 0

tests/rtl/soc_rib2ram_tb.sv

@@ -1,6 +1,6 @@
 `timescale 1ns / 1ps
 
-module soc_rib_ram_tb;
+module soc_rib2ram_tb;
   logic          clk_i = 1'b0;
   logic          rst_n_i = 1'b0;
   logic   [31:0] memory         [0:31];
@@ -19,7 +19,7 @@ module soc_rib_ram_tb;
     if (ram.wstrb[3]) memory[ram.addr][31:24] <= ram.wdata[31:24];
   end
 
-  soc_rib_ram u_dut (
+  soc_rib2ram u_dut (
       .clk_i  (clk_i),
       .rst_n_i(rst_n_i),
       .rib    (rib),

tests/rtl/spill_register_tb.sv

@@ -1,117 +0,0 @@
-`timescale 1ns / 1ps
-
-module spill_register_tb;
-  logic          clk_i = 1'b0;
-  logic          rst_n_i = 1'b0;
-  logic          flush_i = 1'b0;
-  logic          valid_i = 1'b0;
-  logic          ready_o;
-  logic   [31:0] data_i = '0;
-  logic          valid_o;
-  logic          ready_i = 1'b0;
-  logic   [31:0] data_o;
-
-  logic   [31:0] expected             [0:511];
-  integer        head = 0;
-  integer        tail = 0;
-  integer        cycle;
-  logic          held_valid = 1'b0;
-  logic   [31:0] held_data = '0;
-  logic   [31:0] lfsr = 32'h1ACE_B00C;
-
-  always #5 clk_i = ~clk_i;
-
-  spill_register #(
-      .DATA_WIDTH(32),
-      .BYPASS    (1'b0)
-  ) u_dut (
-      .clk_i  (clk_i),
-      .rst_n_i(rst_n_i),
-      .flush_i(flush_i),
-      .valid_i(valid_i),
-      .ready_o(ready_o),
-      .data_i (data_i),
-      .valid_o(valid_o),
-      .ready_i(ready_i),
-      .data_o (data_o)
-  );
-
-  task automatic check_cycle;
-    begin
-      @(posedge clk_i);
-      if (held_valid && !flush_i && (!valid_o || (data_o !== held_data))) begin
-        $fatal(1, "spill register changed output while stalled");
-      end
-      if (valid_o && ready_i) begin
-        if (head == tail || data_o !== expected[head]) begin
-          $fatal(1, "spill register output ordering failure");
-        end
-        head = head + 1;
-      end
-      if (valid_i && ready_o) begin
-        expected[tail] = data_i;
-        tail           = tail + 1;
-      end
-      if (flush_i) begin
-        head = tail;
-      end
-      held_valid = valid_o && !ready_i && !flush_i;
-      held_data  = data_o;
-    end
-  endtask
-
-  initial begin
-    repeat (2) @(posedge clk_i);
-    @(negedge clk_i);
-    rst_n_i = 1'b1;
-
-    // Sustained one-word-per-cycle traffic exercises simultaneous push/pop.
-    for (cycle = 0; cycle < 16; cycle = cycle + 1) begin
-      valid_i = 1'b1;
-      ready_i = 1'b1;
-      data_i  = 32'h1000_0000 + cycle;
-      check_cycle();
-      @(negedge clk_i);
-    end
-
-    // Fill both entries, hold the output, and check stability under pressure.
-    ready_i = 1'b0;
-    for (cycle = 0; cycle < 8; cycle = cycle + 1) begin
-      valid_i = 1'b1;
-      data_i  = 32'h2000_0000 + cycle;
-      check_cycle();
-      @(negedge clk_i);
-    end
-
-    valid_i = 1'b1;
-    data_i  = 32'hDEAD_BEEF;
-    flush_i = 1'b1;
-    check_cycle();
-    if (valid_o || ready_o) begin
-      $fatal(1, "spill register accepted a transfer while flushing");
-    end
-    @(negedge clk_i);
-    flush_i = 1'b0;
-
-    // Deterministic randomized backpressure covers all occupancy transitions.
-    for (cycle = 0; cycle < 256; cycle = cycle + 1) begin
-      lfsr    = {lfsr[30:0], lfsr[31] ^ lfsr[21] ^ lfsr[1] ^ lfsr[0]};
-      valid_i = lfsr[0] | lfsr[3];
-      ready_i = lfsr[1] | lfsr[5];
-      data_i  = 32'h3000_0000 + cycle;
-      check_cycle();
-      @(negedge clk_i);
-    end
-
-    valid_i = 1'b0;
-    ready_i = 1'b1;
-    while (head != tail || valid_o) begin
-      check_cycle();
-      @(negedge clk_i);
-    end
-
-    $display("spill register ready/valid test passed");
-    $finish;
-  end
-
-endmodule

tests/rtl/tc_pdk_cells_tb.sv

@@ -74,12 +74,12 @@ module tc_pdk_cells_tb;
 `endif
 
 `ifdef PDK_ICS55
-  logic ics55_od_i;
-  logic ics55_od_oe;
-  logic ics55_od_mode;
-  logic ics55_pu;
-  logic ics55_pd;
-  tri   ics55_pad;
+  logic       ics55_od_i;
+  logic       ics55_od_oe;
+  logic       ics55_od_mode;
+  logic       ics55_pu;
+  logic       ics55_pd;
+  tri         ics55_pad;
   logic [2:0] ics55_mux_inputs;
   logic       ics55_mux_y;
 
@@ -202,11 +202,11 @@ module tc_pdk_cells_tb;
     gf180_seq_reset_n = 1'b0;
 `endif
 `ifdef PDK_ICS55
-    ics55_od_i    = 1'b1;
-    ics55_od_oe   = 1'b0;
-    ics55_od_mode = 1'b1;
-    ics55_pu      = 1'b0;
-    ics55_pd      = 1'b0;
+    ics55_od_i       = 1'b1;
+    ics55_od_oe      = 1'b0;
+    ics55_od_mode    = 1'b1;
+    ics55_pu         = 1'b0;
+    ics55_pd         = 1'b0;
     ics55_mux_inputs = 3'b000;
 `endif
 
@@ -309,11 +309,8 @@ module tc_pdk_cells_tb;
     for (int mux_vector = 0; mux_vector < 8; mux_vector++) begin
       ics55_mux_inputs = mux_vector[2:0];
       #1;
-      expect_bit(
-          ics55_mux_y,
-          ~(ics55_mux_inputs[2] ? ics55_mux_inputs[1] : ics55_mux_inputs[0]),
-          $sformatf("ICS55 MUXI2 vector %0d", mux_vector)
-      );
+      expect_bit(ics55_mux_y, ~(ics55_mux_inputs[2] ? ics55_mux_inputs[1] : ics55_mux_inputs[0]),
+                 $sformatf("ICS55 MUXI2 vector %0d", mux_vector));
     end
 `endif
 

tests/test_memory_map.py

@@ -121,7 +121,7 @@ def test_bus_fault_responder_handles_reserved_and_unmapped_addresses(tmp_path: P
                 str(ROOT / "rtl/mini/top/soc_ribl2rib.sv"),
                 str(ROOT / "rtl/mini/top/soc_rib2ribp.sv"),
                 str(ROOT / "rtl/mini/top/soc_rib_error_slave.sv"),
-                str(ROOT / "rtl/mini/top/soc_rib_ram.sv"),
+                str(ROOT / "rtl/mini/top/soc_rib2ram.sv"),
                 str(ROOT / "rtl/mini/top/bus.sv"),
                 str(ROOT / "tests/rtl/bus_fault_tb.sv"),
                 "",

tests/test_rib.py

@@ -48,7 +48,7 @@ def test_bus_preserves_incr4_and_rejects_illegal_bursts(tmp_path: Path) -> None:
                 str(ROOT / "rtl/mini/top/soc_ribl2rib.sv"),
                 str(ROOT / "rtl/mini/top/soc_rib2ribp.sv"),
                 str(ROOT / "rtl/mini/top/soc_rib_error_slave.sv"),
-                str(ROOT / "rtl/mini/top/soc_rib_ram.sv"),
+                str(ROOT / "rtl/mini/top/soc_rib2ram.sv"),
                 str(ROOT / "rtl/mini/top/bus.sv"),
                 str(ROOT / "tests/rtl/rib_bus_tb.sv"),
                 "",
@@ -77,37 +77,13 @@ def test_bus_preserves_incr4_and_rejects_illegal_bursts(tmp_path: Path) -> None:
     assert "RIB burst arbitration and protocol test passed" in result.stdout
 
 
-def test_common_spill_register_preserves_ready_valid_data(tmp_path: Path) -> None:
-    iverilog = shutil.which("iverilog")
-    vvp = shutil.which("vvp")
-    if iverilog is None or vvp is None:
-        return
-
-    simulation = tmp_path / "spill_register_tb"
-    subprocess.run(
-        [
-            iverilog,
-            "-g2012",
-            "-s",
-            "spill_register_tb",
-            "-o",
-            str(simulation),
-            str(ROOT / "rtl/managed/clusterip/common/rtl/utils/spill_register.sv"),
-            str(ROOT / "tests/rtl/spill_register_tb.sv"),
-        ],
-        check=True,
-    )
-    result = subprocess.run([vvp, str(simulation)], text=True, capture_output=True, check=True)
-    assert "spill register ready/valid test passed" in result.stdout
-
-
 def test_burst_sram_preserves_data_and_backpressure(tmp_path: Path) -> None:
     iverilog = shutil.which("iverilog")
     vvp = shutil.which("vvp")
     if iverilog is None or vvp is None:
         return
 
-    source_list = tmp_path / "soc_rib_ram.fl"
+    source_list = tmp_path / "soc_rib2ram.fl"
     source_list.write_text(
         "\n".join(
             [
@@ -118,14 +94,14 @@ def test_burst_sram_preserves_data_and_backpressure(tmp_path: Path) -> None:
                 str(ROOT / "rtl/mini/top/soc_rib_if.sv"),
                 str(ROOT / "rtl/managed/clusterip/common/rtl/utils/register.sv"),
                 str(ROOT / "rtl/managed/clusterip/common/rtl/utils/spill_register.sv"),
-                str(ROOT / "rtl/mini/top/soc_rib_ram.sv"),
-                str(ROOT / "tests/rtl/soc_rib_ram_tb.sv"),
+                str(ROOT / "rtl/mini/top/soc_rib2ram.sv"),
+                str(ROOT / "tests/rtl/soc_rib2ram_tb.sv"),
                 "",
             ]
         ),
         encoding="utf-8",
     )
-    converted = tmp_path / "soc_rib_ram_tb.v"
+    converted = tmp_path / "soc_rib2ram_tb.v"
     subprocess.run(
         [
             sys.executable,
@@ -137,9 +113,9 @@ def test_burst_sram_preserves_data_and_backpressure(tmp_path: Path) -> None:
         ],
         check=True,
     )
-    simulation = tmp_path / "soc_rib_ram_tb"
+    simulation = tmp_path / "soc_rib2ram_tb"
     subprocess.run(
-        [iverilog, "-g2012", "-s", "soc_rib_ram_tb", "-o", str(simulation), str(converted)],
+        [iverilog, "-g2012", "-s", "soc_rib2ram_tb", "-o", str(simulation), str(converted)],
         check=True,
     )
     result = subprocess.run([vvp, str(simulation)], text=True, capture_output=True, check=True)

tests/test_script_tools.py

@@ -181,7 +181,6 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
 
     bus_filelist = tmp_path / "bus.fl"
     rib_adapter_filelist = tmp_path / "rib_adapter.fl"
-    spill_register_filelist = tmp_path / "spill_register.fl"
     rib2apb_filelist = tmp_path / "ribp2apb.fl"
     sysctrl_filelist = tmp_path / "sysctrl.fl"
     pll_rcu_filelist = tmp_path / "pll_rcu.fl"
@@ -190,9 +189,6 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
     assert generate_formal_filelist(
         "rib_adapter", rib_adapter_filelist, memory_map, topology, user_extensions
     )
-    assert generate_formal_filelist(
-        "spill_register", spill_register_filelist, memory_map, topology, user_extensions
-    )
     assert generate_formal_filelist(
         "ribp2apb", rib2apb_filelist, memory_map, topology, user_extensions
     )
@@ -208,7 +204,6 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
 
     bus = parse_filelists([bus_filelist], require_files=False)
     rib_adapter = parse_filelists([rib_adapter_filelist], require_files=False)
-    spill_register = parse_filelists([spill_register_filelist], require_files=False)
     ribp2apb = parse_filelists([rib2apb_filelist], require_files=False)
     sysctrl = parse_filelists([sysctrl_filelist], require_files=False)
     pll_rcu = parse_filelists([pll_rcu_filelist], require_files=False)
@@ -221,11 +216,6 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
     assert ROOT / "rtl/mini/formal/bus_formal.sv" in bus.files
     assert ROOT / "rtl/mini/top/soc_rib2ribp.sv" in rib_adapter.files
     assert ROOT / "rtl/mini/formal/rib_adapter_formal.sv" in rib_adapter.files
-    assert (
-        ROOT / "rtl/managed/clusterip/common/rtl/utils/spill_register.sv"
-        in spill_register.files
-    )
-    assert ROOT / "rtl/mini/formal/spill_register_formal.sv" in spill_register.files
     assert ROOT / "rtl/ip/ribp/interconnect/ribp2apb.sv" in ribp2apb.files
     assert ROOT / "rtl/mini/formal/ribp2apb_formal.sv" in ribp2apb.files
     assert ROOT / "rtl/managed/clusterip/common/rtl/interface/apb4_pure_if.sv" in ribp2apb.files
@@ -233,6 +223,7 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
     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/managed/clusterip/common/rtl/clkrst/rst_sync.sv" in pll_rcu.files
     assert ROOT / "rtl/ip/ribp/peripheral/gpio.sv" in gpio_user.files
     assert ROOT / "rtl/managed/clusterip/common/rtl/cdc/cdc_sync.sv" in gpio_user.files
     assert ROOT / "rtl/mini/formal/gpio_user_formal.sv" in gpio_user.files
@@ -548,6 +539,7 @@ def test_format_file_scope_is_tracked_and_self_owned() -> None:
         Path("rtl/ip/ribp/peripheral/sysctrl.sv"),
         Path("rtl/tech/tc_clk.sv"),
         Path("rtl/demo/reference.v"),
+        Path("tests/rtl/bus_fault_tb.sv"),
         Path("rtl/managed/clusterip/common/rtl/utils/register.sv"),
         Path("rtl/managed/third_party/core.v"),
         Path("rtl/mini/filelist.f"),
@@ -562,6 +554,7 @@ def test_format_file_scope_is_tracked_and_self_owned() -> None:
         Path("rtl/ip/ribp/peripheral/sysctrl.sv"),
         Path("rtl/mini/top/retrosoc.sv"),
         Path("rtl/tech/tc_clk.sv"),
+        Path("tests/rtl/bus_fault_tb.sv"),
     ]
 
 

tests/test_soc_topology.py

@@ -147,7 +147,7 @@ def test_topology_always_adds_the_user_apb_target(tmp_path: Path) -> None:
     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/ribp2apb_formal.sv").read_text(encoding="utf-8")
-    formal_properties = (ROOT / "rtl/mini/formal/ribp2apb_formal_props.v").read_text(
+    formal_properties = (ROOT / "rtl/mini/formal/ribp2apb_formal_props.sv").read_text(
         encoding="utf-8"
     )